--- 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 \<equiv> List.member xs x"
--- 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
--- 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"
--- 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
--- 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 *)
--- 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
--- 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"
--- 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
*}
--- 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 *