src/HOL/Integ/Presburger.thy
changeset 15013 34264f5e4691
parent 14981 e73f8140af78
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Integ/Presburger.thy	Wed Jun 30 14:04:58 2004 +0200
     1.2 +++ b/src/HOL/Integ/Presburger.thy	Thu Jul 01 12:29:53 2004 +0200
     1.3 @@ -969,7 +969,7 @@
     1.4  theorem number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (n BIT b)"
     1.5    by simp
     1.6  
     1.7 -theorem number_of2: "(0::int) <= number_of bin.Pls" by simp
     1.8 +theorem number_of2: "(0::int) <= Numeral0" by simp
     1.9  
    1.10  theorem Suc_plus1: "Suc n = n + 1" by simp
    1.11