summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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