# HG changeset patch
# User haftmann
# Date 1330815284 -3600
# Node ID f21494dc0bf670bf184e5d01667390c2e278623d
# Parent  9ae5c21fc88c70c5a9cbc337766377fa08aca4af
generalized user-visible text

diff -r 9ae5c21fc88c -r f21494dc0bf6 src/HOL/Import/README
--- 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.
diff -r 9ae5c21fc88c -r f21494dc0bf6 src/HOL/Import/import.ML
--- 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
 
diff -r 9ae5c21fc88c -r f21494dc0bf6 src/HOL/Import/import_rews.ML
--- 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
diff -r 9ae5c21fc88c -r f21494dc0bf6 src/HOL/Import/import_syntax.ML
--- 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