--- 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>
--- 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.
*)
--- 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.
--- 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)
--- 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 =