changeset 764 | a603aa6c9d01 |
parent 762 | baac4639ecef |
child 766 | df053507edba |
--- a/Quot/Examples/IntEx.thy Sat Dec 19 22:42:31 2009 +0100 +++ b/Quot/Examples/IntEx.thy Sun Dec 20 00:14:46 2009 +0100 @@ -100,7 +100,7 @@ where "SIGN i = (if i = ZERO then ZERO else if (LESS ZERO i) then ONE else (NEG ONE))" -ML {* Quotient_Info.print_qconstinfo @{context} *} +print_quotconsts lemma plus_sym_pre: shows "my_plus a b \<approx> my_plus b a"