# HG changeset patch # User haftmann # Date 1330814601 -3600 # Node ID 81e5ec0a3cd0d1bf21dcfda5d861c1dc9f37c534 # Parent 72c77ea184e628fe0e59d6282cbbf09a196ccfdc one unified Importer theory diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL4/Compatibility.thy --- a/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL4/Compatibility.thy Sat Mar 03 23:43:21 2012 +0100 @@ -7,7 +7,7 @@ Complex_Main "~~/src/HOL/Old_Number_Theory/Primes" "~~/src/HOL/Library/ContNotDenum" - "~~/src/HOL/Import/HOL4Syntax" + "~~/src/HOL/Import/Importer" begin abbreviation (input) mem (infixl "mem" 55) where "x mem xs \ List.member xs x" diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL4/Generated/HOL4Base.thy --- a/src/HOL/Import/HOL4/Generated/HOL4Base.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL4/Generated/HOL4Base.thy Sat Mar 03 23:43:21 2012 +0100 @@ -1,7 +1,7 @@ (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) theory HOL4Base -imports "../../HOL4Syntax" "../Compatibility" +imports "../../Importer" "../Compatibility" begin setup_theory "~~/src/HOL/Import/HOL4/Generated" bool diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL4/Generated/bool.imp --- a/src/HOL/Import/HOL4/Generated/bool.imp Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL4/Generated/bool.imp Sat Mar 03 23:43:21 2012 +0100 @@ -18,14 +18,14 @@ "~" > "HOL.Not" "bool_case" > "Product_Type.bool.bool_case" "\\/" > "HOL.disj" - "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" + "TYPE_DEFINITION" > "Importer.TYPE_DEFINITION" "T" > "HOL.True" "RES_SELECT" > "HOL4Base.bool.RES_SELECT" "RES_FORALL" > "HOL4Base.bool.RES_FORALL" "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE" "RES_EXISTS" > "HOL4Base.bool.RES_EXISTS" "ONTO" > "Fun.surj" - "ONE_ONE" > "HOL4Setup.ONE_ONE" + "ONE_ONE" > "Importer.ONE_ONE" "LET" > "Compatibility.LET" "IN" > "HOL4Base.bool.IN" "F" > "HOL.False" @@ -49,14 +49,14 @@ "UEXISTS_SIMP" > "HOL4Base.bool.UEXISTS_SIMP" "UEXISTS_OR_THM" > "HOL4Base.bool.UEXISTS_OR_THM" "T_DEF" > "HOL.True_def" - "TYPE_DEFINITION_THM" > "HOL4Setup.TYPE_DEFINITION" - "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION" + "TYPE_DEFINITION_THM" > "Importer.TYPE_DEFINITION" + "TYPE_DEFINITION" > "Importer.TYPE_DEFINITION" "TRUTH" > "HOL.TrueI" "SWAP_FORALL_THM" > "HOL.all_comm" "SWAP_EXISTS_THM" > "HOL.ex_comm" "SKOLEM_THM" > "HOL4Base.bool.SKOLEM_THM" "SELECT_UNIQUE" > "HOL4Base.bool.SELECT_UNIQUE" - "SELECT_THM" > "HOL4Setup.EXISTS_DEF" + "SELECT_THM" > "Importer.EXISTS_DEF" "SELECT_REFL_2" > "Hilbert_Choice.some_sym_eq_trivial" "SELECT_REFL" > "Hilbert_Choice.some_eq_trivial" "SELECT_AX" > "Hilbert_Choice.someI" @@ -88,7 +88,7 @@ "ONTO_THM" > "Fun.surj_def" "ONTO_DEF" > "Fun.surj_def" "ONE_ONE_THM" > "HOL4Base.bool.ONE_ONE_THM" - "ONE_ONE_DEF" > "HOL4Setup.ONE_ONE_DEF" + "ONE_ONE_DEF" > "Importer.ONE_ONE_DEF" "NOT_IMP" > "HOL.not_imp" "NOT_FORALL_THM" > "HOL.not_all" "NOT_F" > "Groebner_Basis.PFalse_2" @@ -118,7 +118,7 @@ "LEFT_AND_FORALL_THM" > "HOL.all_simps_1" "IN_def" > "HOL4Base.bool.IN_def" "IN_DEF" > "HOL4Base.bool.IN_DEF" - "INFINITY_AX" > "HOL4Setup.INFINITY_AX" + "INFINITY_AX" > "Importer.INFINITY_AX" "IMP_F_EQ_F" > "HOL4Base.bool.IMP_F_EQ_F" "IMP_F" > "HOL.notI" "IMP_DISJ_THM" > "Groebner_Basis.nnf_simps_3" @@ -140,7 +140,7 @@ "EXISTS_SIMP" > "HOL.simp_thms_36" "EXISTS_REFL" > "HOL.simp_thms_37" "EXISTS_OR_THM" > "HOL.ex_disj_distrib" - "EXISTS_DEF" > "HOL4Setup.EXISTS_DEF" + "EXISTS_DEF" > "Importer.EXISTS_DEF" "EXCLUDED_MIDDLE" > "HOL4Base.bool.EXCLUDED_MIDDLE" "ETA_THM" > "HOL.eta_contract_eq" "ETA_AX" > "HOL.eta_contract_eq" diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL4/Template/GenHOL4Base.thy --- a/src/HOL/Import/HOL4/Template/GenHOL4Base.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL4/Template/GenHOL4Base.thy Sat Mar 03 23:43:21 2012 +0100 @@ -3,7 +3,7 @@ *) theory GenHOL4Base -imports "../../HOL4Syntax" "../Compatibility" +imports "../../Importer" "../Compatibility" begin import_segment "hol4" @@ -11,7 +11,7 @@ setup_dump "../Generated" "HOL4Base" append_dump {*theory HOL4Base -imports "../../HOL4Syntax" "../Compatibility" +imports "../../Importer" "../Compatibility" begin *} @@ -31,9 +31,9 @@ "~" > HOL.Not COND > HOL.If bool_case > Product_Type.bool.bool_case - ONE_ONE > HOL4Setup.ONE_ONE + ONE_ONE > Importer.ONE_ONE ONTO > Fun.surj - TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION + TYPE_DEFINITION > Importer.TYPE_DEFINITION LET > Compatibility.LET; ignore_thms diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL_Light/Compatibility.thy --- a/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Compatibility.thy Sat Mar 03 23:43:21 2012 +0100 @@ -5,7 +5,7 @@ theory Compatibility imports Main Fact Parity "~~/src/HOL/Library/Infinite_Set" - HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/HOL4Syntax" + HOLLightList HOLLightReal HOLLightInt "~~/src/HOL/Import/Importer" begin (* list *) diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL_Light/Generated/HOLLight.thy --- a/src/HOL/Import/HOL_Light/Generated/HOLLight.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Generated/HOLLight.thy Sat Mar 03 23:43:21 2012 +0100 @@ -1,7 +1,7 @@ (* AUTOMATICALLY GENERATED, DO NOT EDIT! *) theory HOLLight -imports "../../HOL4Syntax" "../Compatibility" +imports "../../Importer" "../Compatibility" begin setup_theory "~~/src/HOL/Import/HOL_Light/Generated" hollight diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL_Light/Generated/hollight.imp --- a/src/HOL/Import/HOL_Light/Generated/hollight.imp Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Generated/hollight.imp Sat Mar 03 23:43:21 2012 +0100 @@ -528,7 +528,7 @@ "cth" > "HOLLight.hollight.cth" "bool_RECURSION" > "HOLLight.hollight.bool_RECURSION" "bool_INDUCT" > "Product_Type.bool.induct" - "ax__3" > "HOL4Setup.INFINITY_AX" + "ax__3" > "Importer.INFINITY_AX" "ax__2" > "Hilbert_Choice.someI" "ax__1" > "HOL.eta_contract_eq" "admissible_def" > "HOLLight.hollight.admissible_def" @@ -1797,7 +1797,7 @@ "EXISTS_UNIQUE" > "HOL.Ex1_def" "EXISTS_UNCURRY" > "HOLLight.hollight.EXISTS_UNCURRY" "EXISTS_TRIPLED_THM" > "HOLLight.hollight.EXISTS_TRIPLED_THM" - "EXISTS_THM" > "HOL4Setup.EXISTS_DEF" + "EXISTS_THM" > "Importer.EXISTS_DEF" "EXISTS_SUBSET_IMAGE" > "HOLLight.hollight.EXISTS_SUBSET_IMAGE" "EXISTS_SIMP" > "HOL.simp_thms_36" "EXISTS_REFL" > "HOL.simp_thms_37" diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/HOL_Light/Template/GenHOLLight.thy --- a/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/HOL_Light/Template/GenHOLLight.thy Sat Mar 03 23:43:21 2012 +0100 @@ -4,7 +4,7 @@ *) theory GenHOLLight -imports "../../HOL4Syntax" "../Compatibility" +imports "../../Importer" "../Compatibility" begin import_segment "hollight" @@ -12,7 +12,7 @@ setup_dump "../Generated" "HOLLight" append_dump {*theory HOL4Base -imports "../../HOL4Syntax" "../Compatibility" +imports "../../Importer" "../Compatibility" begin *} diff -r 72c77ea184e6 -r 81e5ec0a3cd0 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Mar 03 23:42:56 2012 +0100 +++ b/src/HOL/Import/proof_kernel.ML Sat Mar 03 23:43:21 2012 +0100 @@ -936,7 +936,7 @@ val trans_thm = @{thm trans} val symmetry_thm = @{thm sym} val eqmp_thm = @{thm iffD1} -val eqimp_thm = @{thm HOL4Setup.eq_imp} +val eqimp_thm = @{thm Importer.eq_imp} val comb_thm = @{thm cong} (* Beta-eta normalizes a theorem (only the conclusion, not the *