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/bool.imp
changeset 15647 b1f486a9c56b
parent 14516 a183dec876ab
child 16587 b34c8aa657a5 
--- a/src/HOL/Import/HOL/bool.imp	Fri Apr 01 18:40:14 2005 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Fri Apr 01 18:59:17 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" > "Set.bool_induct"
+  "bool_INDUCT" > "Datatype.bool.induct"
   "boolAxiom" > "HOL4Base.bool.boolAxiom"
   "UNWIND_THM2" > "HOL.simp_thms_39"
   "UNWIND_THM1" > "HOL.simp_thms_40"
@@ -78,7 +78,7 @@
   "OR_INTRO_THM2" > "HOL.disjI2"
   "OR_INTRO_THM1" > "HOL.disjI1"
   "OR_IMP_THM" > "HOL4Base.bool.OR_IMP_THM"
-  "OR_ELIM_THM" > "Recdef.tfl_disjE"
+  "OR_ELIM_THM" > "HOL.disjE"
   "OR_DEF" > "HOL.or_def"
   "OR_CONG" > "HOL4Base.bool.OR_CONG"
   "OR_CLAUSES" > "HOL4Base.bool.OR_CLAUSES"
@@ -93,10 +93,10 @@
   "NOT_DEF" > "HOL.simp_thms_19"
   "NOT_CLAUSES" > "HOL4Base.bool.NOT_CLAUSES"
   "NOT_AND" > "HOL4Base.bool.NOT_AND"
-  "MONO_OR" > "Inductive.basic_monos_3"
+  "MONO_OR" > "Sum_Type.basic_monos_3"
   "MONO_NOT" > "HOL.rev_contrapos"
   "MONO_IMP" > "Set.imp_mono"
-  "MONO_EXISTS" > "Inductive.basic_monos_5"
+  "MONO_EXISTS" > "Sum_Type.basic_monos_5"
   "MONO_COND" > "HOL4Base.bool.MONO_COND"
   "MONO_AND" > "Hilbert_Choice.conj_forward"
   "MONO_ALL" > "Inductive.basic_monos_6"
@@ -139,12 +139,12 @@
   "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
   "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
   "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
-  "ETA_THM" > "Presburger.fm_modd_pinf"
-  "ETA_AX" > "Presburger.fm_modd_pinf"
+  "ETA_THM" > "HOL.eta_contract_eq"
+  "ETA_AX" > "HOL.eta_contract_eq"
   "EQ_TRANS" > "Set.basic_trans_rules_31"
   "EQ_SYM_EQ" > "HOL.eq_sym_conv"
   "EQ_SYM" > "HOL.meta_eq_to_obj_eq"
-  "EQ_REFL" > "Presburger.fm_modd_pinf"
+  "EQ_REFL" > "HOL.refl"
   "EQ_IMP_THM" > "HOL.iff_conv_conj_imp"
   "EQ_EXT" > "HOL.meta_eq_to_obj_eq"
   "EQ_EXPAND" > "HOL4Base.bool.EQ_EXPAND"
@@ -152,7 +152,7 @@
   "DISJ_SYM" > "HOL.disj_comms_1"
   "DISJ_IMP_THM" > "HOL.imp_disjL"
   "DISJ_COMM" > "HOL.disj_comms_1"
-  "DISJ_ASSOC" > "Recdef.tfl_disj_assoc"
+  "DISJ_ASSOC" > "HOL.disj_assoc"
   "DE_MORGAN_THM" > "HOL4Base.bool.DE_MORGAN_THM"
   "CONJ_SYM" > "HOL.conj_comms_1"
   "CONJ_COMM" > "HOL.conj_comms_1"
@@ -172,8 +172,8 @@
   "BOOL_FUN_INDUCT" > "HOL4Base.bool.BOOL_FUN_INDUCT"
   "BOOL_FUN_CASES_THM" > "HOL4Base.bool.BOOL_FUN_CASES_THM"
   "BOOL_EQ_DISTINCT" > "HOL4Base.bool.BOOL_EQ_DISTINCT"
-  "BOOL_CASES_AX" > "HOL.True_or_False"
-  "BETA_THM" > "Presburger.fm_modd_pinf"
+  "BOOL_CASES_AX" > "Datatype.bool.nchotomy"
+  "BETA_THM" > "HOL.eta_contract_eq"
   "ARB_def" > "HOL4Base.bool.ARB_def"
   "ARB_DEF" > "HOL4Base.bool.ARB_DEF"
   "AND_INTRO_THM" > "HOL.conjI"
@@ -183,7 +183,7 @@
   "AND_CLAUSES" > "HOL4Base.bool.AND_CLAUSES"
   "AND2_THM" > "HOL.conjunct2"
   "AND1_THM" > "HOL.conjunct1"
-  "ABS_SIMP" > "Presburger.fm_modd_pinf"
+  "ABS_SIMP" > "HOL.refl"
   "ABS_REP_THM" > "HOL4Base.bool.ABS_REP_THM"
 
 ignore_thms
isabelle