changeset 588 | 2c95d0436a2b |
parent 585 | b16cac0b7c88 |
--- a/IntEx2.thy Mon Dec 07 00:13:36 2009 +0100 +++ b/IntEx2.thy Mon Dec 07 01:22:20 2009 +0100 @@ -389,6 +389,7 @@ "_Numeral" :: "num_const \<Rightarrow> 'a" ("_") use "~~/src/HOL/Tools/numeral_syntax.ML" +(* setup NumeralSyntax.setup abbreviation @@ -432,3 +433,4 @@ lemmas normalize_bin_simps = Bit0_Pls Bit1_Min +*) \ No newline at end of file