# HG changeset patch
# User wenzelm
# Date 1737410417 -3600
# Node ID cb05f8d3fd0503219d9b72b48e317a6af35058f6
# Parent  0a1ed07a458a39220dd2fa69f1cf8b30848242c6
more comments;
more authors;

diff -r 0a1ed07a458a -r cb05f8d3fd05 src/HOL/Import/Import_Setup.thy
--- a/src/HOL/Import/Import_Setup.thy	Mon Jan 20 22:53:51 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy	Mon Jan 20 23:00:17 2025 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Import/Import_Setup.thy
     Author:     Cezary Kaliszyk, University of Innsbruck
     Author:     Alexander Krauss, QAware GmbH
+    Author:     Makarius
 *)
 
 section \<open>Importer machinery\<close>
diff -r 0a1ed07a458a -r cb05f8d3fd05 src/HOL/Import/import_data.ML
--- a/src/HOL/Import/import_data.ML	Mon Jan 20 22:53:51 2025 +0100
+++ b/src/HOL/Import/import_data.ML	Mon Jan 20 23:00:17 2025 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Import/import_data.ML
     Author:     Cezary Kaliszyk, University of Innsbruck
     Author:     Alexander Krauss, QAware GmbH
+    Author:     Makarius
 
 Importer data.
 *)
diff -r 0a1ed07a458a -r cb05f8d3fd05 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Mon Jan 20 22:53:51 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Mon Jan 20 23:00:17 2025 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/Import/import_rule.ML
     Author:     Cezary Kaliszyk, University of Innsbruck
     Author:     Alexander Krauss, QAware GmbH
+    Author:     Makarius
 
 Importer proof rules and processing of lines and files.
 
diff -r 0a1ed07a458a -r cb05f8d3fd05 src/HOL/Import/offline/README
--- a/src/HOL/Import/offline/README	Mon Jan 20 22:53:51 2025 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,12 +0,0 @@
-* Compile and run "offline/offline.ml" (warning, this uses a lot of memory)
-
-  ocamlopt offline.ml -o offline
-  > maps.lst
-  ./offline
-
-* Format of maps.lst:
-
-  - THM1 THM2   map HOL Light THM1 to Isabelle/HOL THM2 and forget its deps
-  - THM -       do not record THM and make sure it is not used (its deps must be mapped)
-  - THM         the definition of constant/type is mapped in Isabelle/HOL, so forget
-                its deps and look its map up when defining (may fail at import time)
diff -r 0a1ed07a458a -r cb05f8d3fd05 src/HOL/Import/offline/offline.ml
--- a/src/HOL/Import/offline/offline.ml	Mon Jan 20 22:53:51 2025 +0100
+++ b/src/HOL/Import/offline/offline.ml	Mon Jan 20 23:00:17 2025 +0100
@@ -1,3 +1,29 @@
+(*  Title:      HOL/Import/offline/offline.ml
+    Author:     Cezary Kaliszyk, University of Innsbruck
+    Author:     Alexander Krauss, QAware GmbH
+
+Stand-alone OCaml program for post-processing of HOL Light export:
+
+  - input files: facts.lst, maps.lst, proofs
+  - output files: facts.lstN, proofsN
+
+Compile and run "offline/offline.ml" like this:
+
+  ocamlopt offline.ml -o offline
+  > maps.lst
+  ./offline   # this uses a lot of memory
+
+Format of maps.lst:
+
+  THM1 THM2
+    map HOL Light THM1 to Isabelle/HOL THM2 and forget its deps
+  THM -
+    do not record THM and make sure it is not used (its deps must be mapped)
+  THM
+    the definition of constant/type is mapped in Isabelle/HOL, so forget
+    its deps and look its map up when defining (may fail at import time)
+*)
+
 let output_int oc i = output_string oc (string_of_int i);;
 let string_list_of_string str sep =
   let rec slos_aux str ans =