diff -r e2ac18492c68 -r baac4639ecef Quot/Examples/IntEx.thy --- a/Quot/Examples/IntEx.thy Sat Dec 19 22:09:57 2009 +0100 +++ b/Quot/Examples/IntEx.thy Sat Dec 19 22:21:51 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 {* print_qconstinfo @{context} *} +ML {* Quotient_Info.print_qconstinfo @{context} *} lemma plus_sym_pre: shows "my_plus a b \ my_plus b a"