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.
updated;
authorwenzelm
Tue, 18 Oct 2005 17:59:22 +0200
changeset 17889 29391114c295
parent 17888 116a8d1c7a67
child 17890 fddb41d3cfa5
updated;
src/HOL/Import/HOL/bool.imp file | annotate | diff | comparison | revisions
src/HOL/Import/HOL/pair.imp file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/HOL/bool.imp	Tue Oct 18 15:08:38 2005 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Tue Oct 18 17:59:22 2005 +0200
@@ -37,7 +37,7 @@
   "bool_case_thm" > "HOL4Base.bool.bool_case_thm"
   "bool_case_ID" > "HOL4Base.bool.bool_case_ID"
   "bool_case_DEF" > "HOL4Compat.bool_case_DEF"
-  "bool_INDUCT" > "Datatype.bool.induct_correctness"
+  "bool_INDUCT" > "Datatype.bool.induct"
   "boolAxiom" > "HOL4Base.bool.boolAxiom"
   "UNWIND_THM2" > "HOL.simp_thms_39"
   "UNWIND_THM1" > "HOL.simp_thms_40"
--- a/src/HOL/Import/HOL/pair.imp	Tue Oct 18 15:08:38 2005 +0200
+++ b/src/HOL/Import/HOL/pair.imp	Tue Oct 18 17:59:22 2005 +0200
@@ -21,7 +21,7 @@
   "##" > "prod_fun"
 
 thm_maps
-  "pair_induction" > "Datatype.prod.induct_correctness"
+  "pair_induction" > "Datatype.prod.induct"
   "pair_case_thm" > "Product_Type.split"
   "pair_case_def" > "HOL4Compat.pair_case_def"
   "pair_case_cong" > "HOL4Base.pair.pair_case_cong"
isabelle