--- a/src/HOL/Import/README Sat Mar 03 23:49:54 2012 +0100
+++ b/src/HOL/Import/README Sat Mar 03 23:54:44 2012 +0100
@@ -11,9 +11,9 @@
HOL-Import-HOL" in ~~/src/HOL.
Note that the quick_and_dirty flag is on as default for this
-directory, which means that the original HOL4 proofs are not consulted
-at all. If a real replay of the HOL4 proofs is desired, get and
-unpack the HOL4 proof objects to somewhere on your harddisk, and set
+directory, which means that the original external proofs are not consulted
+at all. If a real replay of the external proofs is desired, get and
+unpack the external proof objects to somewhere on your harddisk, and set
the variable PROOF_DIRS to the directory where the directory "hol4"
is. Now edit the ROOT.ML file to unset the quick_and_dirty flag and
do "isabelle make HOL-Import-HOL" in ~~/src/HOL.
--- a/src/HOL/Import/import.ML Sat Mar 03 23:49:54 2012 +0100
+++ b/src/HOL/Import/import.ML Sat Mar 03 23:54:44 2012 +0100
@@ -64,7 +64,7 @@
val setup = Method.setup @{binding import}
(Scan.lift (Args.name -- Args.name) >>
(fn arg => fn ctxt => SIMPLE_METHOD (import_tac ctxt arg)))
- "import HOL4 theorem"
+ "import external theorem"
end
--- a/src/HOL/Import/import_rews.ML Sat Mar 03 23:49:54 2012 +0100
+++ b/src/HOL/Import/import_rews.ML Sat Mar 03 23:54:44 2012 +0100
@@ -158,7 +158,7 @@
fun add_hol4_rewrite (Context.Theory thy, th) =
let
- val _ = message "Adding HOL4 rewrite"
+ val _ = message "Adding external rewrite"
val th1 = th RS @{thm eq_reflection}
handle THM _ => th
val current_rews = HOL4Rewrites.get thy
@@ -359,7 +359,7 @@
fun add_hol4_theorem thyname thmname hth =
let
- val _ = message ("Adding HOL4 theorem " ^ thyname ^ "." ^ thmname)
+ val _ = message ("Adding external theorem " ^ thyname ^ "." ^ thmname)
in
HOL4Thms.map (StringPair.update_new ((thyname, thmname), hth))
end;
@@ -634,6 +634,6 @@
val hol4_setup =
initial_maps #>
Attrib.setup @{binding import_rew}
- (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "HOL4 rewrite rule"
+ (Scan.succeed (Thm.mixed_attribute add_hol4_rewrite)) "external rewrite rule"
end
--- a/src/HOL/Import/import_syntax.ML Sat Mar 03 23:49:54 2012 +0100
+++ b/src/HOL/Import/import_syntax.ML Sat Mar 03 23:54:44 2012 +0100
@@ -202,16 +202,16 @@
"Set import segment name"
Keyword.thy_decl (import_segment >> Toplevel.theory);
Outer_Syntax.command "import_theory"
- "Set default HOL4 theory name"
+ "Set default external theory name"
Keyword.thy_decl (import_theory >> Toplevel.theory);
Outer_Syntax.command "end_import"
- "End HOL4 import"
+ "End external import"
Keyword.thy_decl (end_import >> Toplevel.theory);
Outer_Syntax.command "setup_theory"
- "Setup HOL4 theory replaying"
+ "Setup external theory replaying"
Keyword.thy_decl (setup_theory >> Toplevel.theory);
Outer_Syntax.command "end_setup"
- "End HOL4 setup"
+ "End external setup"
Keyword.thy_decl (end_setup >> Toplevel.theory);
Outer_Syntax.command "setup_dump"
"Setup the dump file name"
@@ -223,25 +223,25 @@
"Write the dump to file"
Keyword.thy_decl (fl_dump >> Toplevel.theory);
Outer_Syntax.command "ignore_thms"
- "Theorems to ignore in next HOL4 theory import"
+ "Theorems to ignore in next external theory import"
Keyword.thy_decl (ignore_thms >> Toplevel.theory);
Outer_Syntax.command "type_maps"
- "Map HOL4 type names to existing Isabelle/HOL type names"
+ "Map external type names to existing Isabelle/HOL type names"
Keyword.thy_decl (type_maps >> Toplevel.theory);
Outer_Syntax.command "def_maps"
- "Map HOL4 constant names to their primitive definitions"
+ "Map external constant names to their primitive definitions"
Keyword.thy_decl (def_maps >> Toplevel.theory);
Outer_Syntax.command "thm_maps"
- "Map HOL4 theorem names to existing Isabelle/HOL theorem names"
+ "Map external theorem names to existing Isabelle/HOL theorem names"
Keyword.thy_decl (thm_maps >> Toplevel.theory);
Outer_Syntax.command "const_renames"
- "Rename HOL4 const names"
+ "Rename external const names"
Keyword.thy_decl (const_renames >> Toplevel.theory);
Outer_Syntax.command "const_moves"
- "Rename HOL4 const names to other HOL4 constants"
+ "Rename external const names to other external constants"
Keyword.thy_decl (const_moves >> Toplevel.theory);
Outer_Syntax.command "const_maps"
- "Map HOL4 const names to existing Isabelle/HOL const names"
+ "Map external const names to existing Isabelle/HOL const names"
Keyword.thy_decl (const_maps >> Toplevel.theory));
end