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/prim_rec.imp
changeset 44763 b50d5d694838
parent 35092 cfe605c54e50 
--- a/src/HOL/Import/HOL/prim_rec.imp	Wed Sep 07 00:08:09 2011 +0200
+++ b/src/HOL/Import/HOL/prim_rec.imp	Wed Sep 07 07:59:45 2011 +0900
@@ -18,7 +18,7 @@
   "PRIM_REC_FUN" > "HOL4Base.prim_rec.PRIM_REC_FUN"
   "PRIM_REC" > "HOL4Base.prim_rec.PRIM_REC"
   "PRE" > "HOL4Base.prim_rec.PRE"
-  "<" > "Orderings.less" :: "nat => nat => bool"
+  "<" > "Orderings.ord_class.less" :: "nat => nat => bool"
 
 thm_maps
   "wellfounded_primdef" > "HOL4Base.prim_rec.wellfounded_primdef"
@@ -65,7 +65,7 @@
   "LESS_DEF" > "HOL4Compat.LESS_DEF"
   "LESS_0_0" > "HOL4Base.prim_rec.LESS_0_0"
   "LESS_0" > "Nat.zero_less_Suc"
-  "INV_SUC_EQ" > "Nat.nat.simps_3"
+  "INV_SUC_EQ" > "Nat.nat.inject"
   "EQ_LESS" > "HOL4Base.prim_rec.EQ_LESS"
   "DC" > "HOL4Base.prim_rec.DC"
isabelle