Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOL/arithmetic.imp
changeset 30925 c38cbc0ac8d1
parent 25930 83e3dd60affe
child 31790 05c92381363c 
--- a/src/HOL/Import/HOL/arithmetic.imp	Wed Apr 15 15:30:38 2009 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Apr 15 15:30:39 2009 +0200
@@ -43,7 +43,7 @@
   "TWO" > "HOL4Base.arithmetic.TWO"
   "TIMES2" > "NatSimprocs.nat_mult_2"
   "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
-  "SUC_ONE_ADD" > "NatBin.Suc_eq_add_numeral_1_left"
+  "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_add_numeral_1_left"
   "SUC_NOT" > "Nat.nat.simps_2"
   "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
   "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
@@ -233,7 +233,7 @@
   "EVEN_AND_ODD" > "HOL4Base.arithmetic.EVEN_AND_ODD"
   "EVEN_ADD" > "HOL4Base.arithmetic.EVEN_ADD"
   "EVEN" > "HOL4Base.arithmetic.EVEN"
-  "EQ_MULT_LCANCEL" > "NatBin.nat_mult_eq_cancel_disj"
+  "EQ_MULT_LCANCEL" > "Nat_Numeral.nat_mult_eq_cancel_disj"
   "EQ_MONO_ADD_EQ" > "Nat.nat_add_right_cancel"
   "EQ_LESS_EQ" > "Orderings.order_eq_iff"
   "EQ_ADD_RCANCEL" > "Nat.nat_add_right_cancel"
isabelle