1.1 --- a/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:42:56 2012 +0100
1.2 +++ b/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:43:21 2012 +0100
1.3 @@ -7,7 +7,7 @@
1.4 Complex_Main
1.5 "~~/src/HOL/Old_Number_Theory/Primes"
1.6 "~~/src/HOL/Library/ContNotDenum"
1.7 - "~~/src/HOL/Import/HOL4Syntax"
1.8 + "~~/src/HOL/Import/Importer"
1.9 begin
1.10
1.11 abbreviation (input) mem (infixl "mem" 55) where "x mem xs \<equiv> List.member xs x"
2.1 --- a/src/HOL/Import/HOL4/Generated/HOL4Base.thy Sat Mar 03 23:42:56 2012 +0100
2.2 +++ b/src/HOL/Import/HOL4/Generated/HOL4Base.thy Sat Mar 03 23:43:21 2012 +0100
2.3 @@ -1,7 +1,7 @@
2.4 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
2.5
2.6 theory HOL4Base
2.7 -imports "../../HOL4Syntax" "../Compatibility"
2.8 +imports "../../Importer" "../Compatibility"
2.9 begin
2.10
2.11 setup_theory "~~/src/HOL/Import/HOL4/Generated" bool
3.1 --- a/src/HOL/Import/HOL4/Generated/bool.imp Sat Mar 03 23:42:56 2012 +0100
3.2 +++ b/src/HOL/Import/HOL4/Generated/bool.imp Sat Mar 03 23:43:21 2012 +0100
3.3 @@ -18,14 +18,14 @@
3.4 "~" > "HOL.Not"
3.5 "bool_case" > "Product_Type.bool.bool_case"
3.6 "\\/" > "HOL.disj"
3.7 - "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
3.8 + "TYPE_DEFINITION" > "Importer.TYPE_DEFINITION"
3.9 "T" > "HOL.True"
3.10 "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
3.11 "RES_FORALL" > "HOL4Base.bool.RES_FORALL"
3.12 "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
3.13 "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS"
3.14 "ONTO" > "Fun.surj"
3.15 - "ONE_ONE" > "HOL4Setup.ONE_ONE"
3.16 + "ONE_ONE" > "Importer.ONE_ONE"
3.17 "LET" > "Compatibility.LET"
3.18 "IN" > "HOL4Base.bool.IN"
3.19 "F" > "HOL.False"
3.20 @@ -49,14 +49,14 @@
3.21 "UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP"
3.22 "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM"
3.23 "T_DEF" > "HOL.True_def"
3.24 - "TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION"
3.25 - "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
3.26 + "TYPE_DEFINITION_THM" > "Importer.TYPE_DEFINITION"
3.27 + "TYPE_DEFINITION" > "Importer.TYPE_DEFINITION"
3.28 "TRUTH" > "HOL.TrueI"
3.29 "SWAP_FORALL_THM" > "HOL.all_comm"
3.30 "SWAP_EXISTS_THM" > "HOL.ex_comm"
3.31 "SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM"
3.32 "SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE"
3.33 - "SELECT_THM" > "HOL4Setup.EXISTS_DEF"
3.34 + "SELECT_THM" > "Importer.EXISTS_DEF"
3.35 "SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial"
3.36 "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial"
3.37 "SELECT_AX" > "Hilbert_Choice.someI"
3.38 @@ -88,7 +88,7 @@
3.39 "ONTO_THM" > "Fun.surj_def"
3.40 "ONTO_DEF" > "Fun.surj_def"
3.41 "ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM"
3.42 - "ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF"
3.43 + "ONE_ONE_DEF" > "Importer.ONE_ONE_DEF"
3.44 "NOT_IMP" > "HOL.not_imp"
3.45 "NOT_FORALL_THM" > "HOL.not_all"
3.46 "NOT_F" > "Groebner_Basis.PFalse_2"
3.47 @@ -118,7 +118,7 @@
3.48 "LEFT_AND_FORALL_THM" > "HOL.all_simps_1"
3.49 "IN_def" > "HOL4Base.bool.IN_def"
3.50 "IN_DEF" > "HOL4Base.bool.IN_DEF"
3.51 - "INFINITY_AX" > "HOL4Setup.INFINITY_AX"
3.52 + "INFINITY_AX" > "Importer.INFINITY_AX"
3.53 "IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F"
3.54 "IMP_F" > "HOL.notI"
3.55 "IMP_DISJ_THM" > "Groebner_Basis.nnf_simps_3"
3.56 @@ -140,7 +140,7 @@
3.57 "EXISTS_SIMP" > "HOL.simp_thms_36"
3.58 "EXISTS_REFL" > "HOL.simp_thms_37"
3.59 "EXISTS_OR_THM" > "HOL.ex_disj_distrib"
3.60 - "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF"
3.61 + "EXISTS_DEF" > "Importer.EXISTS_DEF"
3.62 "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE"
3.63 "ETA_THM" > "HOL.eta_contract_eq"
3.64 "ETA_AX" > "HOL.eta_contract_eq"
4.1 --- a/src/HOL/Import/HOL4/Template/GenHOL4Base.thy Sat Mar 03 23:42:56 2012 +0100
4.2 +++ b/src/HOL/Import/HOL4/Template/GenHOL4Base.thy Sat Mar 03 23:43:21 2012 +0100
4.3 @@ -3,7 +3,7 @@
4.4 *)
4.5
4.6 theory GenHOL4Base
4.7 -imports "../../HOL4Syntax" "../Compatibility"
4.8 +imports "../../Importer" "../Compatibility"
4.9 begin
4.10
4.11 import_segment "hol4"
4.12 @@ -11,7 +11,7 @@
4.13 setup_dump "../Generated" "HOL4Base"
4.14
4.15 append_dump {*theory HOL4Base
4.16 -imports "../../HOL4Syntax" "../Compatibility"
4.17 +imports "../../Importer" "../Compatibility"
4.18 begin
4.19 *}
4.20
4.21 @@ -31,9 +31,9 @@
4.22 "~" > HOL.Not
4.23 COND > HOL.If
4.24 bool_case > Product_Type.bool.bool_case
4.25 - ONE_ONE > HOL4Setup.ONE_ONE
4.26 + ONE_ONE > Importer.ONE_ONE
4.27 ONTO > Fun.surj
4.28 - TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
4.29 + TYPE_DEFINITION > Importer.TYPE_DEFINITION
4.30 LET > Compatibility.LET;
4.31
4.32 ignore_thms
5.1 --- a/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:42:56 2012 +0100
5.2 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:43:21 2012 +0100
5.3 @@ -5,7 +5,7 @@
5.4
5.5 theory Compatibility
5.6 imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set"
5.7 - HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/HOL4Syntax"
5.8 + HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/Importer"
5.9 begin
5.10
5.11 (* list *)
6.1 --- a/src/HOL/Import/HOL_Light/Generated/HOLLight.thy Sat Mar 03 23:42:56 2012 +0100
6.2 +++ b/src/HOL/Import/HOL_Light/Generated/HOLLight.thy Sat Mar 03 23:43:21 2012 +0100
6.3 @@ -1,7 +1,7 @@
6.4 (* AUTOMATICALLY GENERATED, DO NOT EDIT! *)
6.5
6.6 theory HOLLight
6.7 -imports "../../HOL4Syntax" "../Compatibility"
6.8 +imports "../../Importer" "../Compatibility"
6.9 begin
6.10
6.11 setup_theory "~~/src/HOL/Import/HOL_Light/Generated" hollight
7.1 --- a/src/HOL/Import/HOL_Light/Generated/hollight.imp Sat Mar 03 23:42:56 2012 +0100
7.2 +++ b/src/HOL/Import/HOL_Light/Generated/hollight.imp Sat Mar 03 23:43:21 2012 +0100
7.3 @@ -528,7 +528,7 @@
7.4 "cth" > "HOLLight.hollight.cth"
7.5 "bool_RECURSION" > "HOLLight.hollight.bool_RECURSION"
7.6 "bool_INDUCT" > "Product_Type.bool.induct"
7.7 - "ax__3" > "HOL4Setup.INFINITY_AX"
7.8 + "ax__3" > "Importer.INFINITY_AX"
7.9 "ax__2" > "Hilbert_Choice.someI"
7.10 "ax__1" > "HOL.eta_contract_eq"
7.11 "admissible_def" > "HOLLight.hollight.admissible_def"
7.12 @@ -1797,7 +1797,7 @@
7.13 "EXISTS_UNIQUE" > "HOL.Ex1_def"
7.14 "EXISTS_UNCURRY" > "HOLLight.hollight.EXISTS_UNCURRY"
7.15 "EXISTS_TRIPLED_THM" > "HOLLight.hollight.EXISTS_TRIPLED_THM"
7.16 - "EXISTS_THM" > "HOL4Setup.EXISTS_DEF"
7.17 + "EXISTS_THM" > "Importer.EXISTS_DEF"
7.18 "EXISTS_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_SUBSET_IMAGE"
7.19 "EXISTS_SIMP" > "HOL.simp_thms_36"
7.20 "EXISTS_REFL" > "HOL.simp_thms_37"
8.1 --- a/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy Sat Mar 03 23:42:56 2012 +0100
8.2 +++ b/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy Sat Mar 03 23:43:21 2012 +0100
8.3 @@ -4,7 +4,7 @@
8.4 *)
8.5
8.6 theory GenHOLLight
8.7 -imports "../../HOL4Syntax" "../Compatibility"
8.8 +imports "../../Importer" "../Compatibility"
8.9 begin
8.10
8.11 import_segment "hollight"
8.12 @@ -12,7 +12,7 @@
8.13 setup_dump "../Generated" "HOLLight"
8.14
8.15 append_dump {*theory HOL4Base
8.16 -imports "../../HOL4Syntax" "../Compatibility"
8.17 +imports "../../Importer" "../Compatibility"
8.18 begin
8.19 *}
8.20
9.1 --- a/src/HOL/Import/proof_kernel.ML Sat Mar 03 23:42:56 2012 +0100
9.2 +++ b/src/HOL/Import/proof_kernel.ML Sat Mar 03 23:43:21 2012 +0100
9.3 @@ -936,7 +936,7 @@
9.4 val trans_thm = @{thm trans}
9.5 val symmetry_thm = @{thm sym}
9.6 val eqmp_thm = @{thm iffD1}
9.7 -val eqimp_thm = @{thm HOL4Setup.eq_imp}
9.8 +val eqimp_thm = @{thm Importer.eq_imp}
9.9 val comb_thm = @{thm cong}
9.10
9.11 (* Beta-eta normalizes a theorem (only the conclusion, not the *