387 

   387 

   388 syntax

   388 syntax

   389   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")

   389   "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")

   390 

   390 

   391 use "~~/src/HOL/Tools/numeral_syntax.ML"

   391 use "~~/src/HOL/Tools/numeral_syntax.ML"

   392 setup NumeralSyntax.setup

   393 setup NumeralSyntax.setup

   393 

   394 

   394 abbreviation

   395 abbreviation

   395   "Numeral0 \<equiv> number_of Pls"

   396   "Numeral0 \<equiv> number_of Pls"

   396 

   397 

   430   "Bit1 Min = Min"

   431   "Bit1 Min = Min"

   431   unfolding numeral_simps by simp

   432   unfolding numeral_simps by simp

   432 

   433 

   433 lemmas normalize_bin_simps =

   434 lemmas normalize_bin_simps =

   434   Bit0_Pls Bit1_Min

   435   Bit0_Pls Bit1_Min