Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
authorhuffman
Tue, 11 May 2010 19:01:35 -0700
changeset 36841 02df88789641
parent 36840 1e020f445846
child 36842 99745a4b9cc9
include iszero_simps in semiring_norm just once (they are already included in rel_simps)
src/HOL/Nat_Numeral.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Nat_Numeral.thy	Tue May 11 19:00:32 2010 -0700
+++ b/src/HOL/Nat_Numeral.thy	Tue May 11 19:01:35 2010 -0700
@@ -712,7 +712,7 @@
   if_True add_0 add_Suc add_number_of_left mult_number_of_left
   numeral_1_eq_1 [symmetric] Suc_eq_plus1
   numeral_0_eq_0 [symmetric] numerals [symmetric]
-  iszero_simps not_iszero_Numeral1
+  not_iszero_Numeral1
 
 lemma Let_Suc [simp]: "Let (Suc n) f == f (Suc n)"
   by (fact Let_def)
isabelle