| author | wenzelm |
| Sat, 18 Jan 2025 22:29:47 +0100 | |
| changeset 81918 | deb6cb34a37f |
| parent 81915 | src/HOL/Import/patches/stage1.patch@02e107686442 |
| child 81919 | f4cd3e679096 |
| permissions | -rw-r--r-- |
|
81915
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
1 |
--- hol-light/statements.ml 1970-01-01 01:00:00.000000000 +0100 |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
2 |
+++ hol-light-patched/statements.ml 2025-01-18 11:12:11.185279392 +0100 |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
3 |
@@ -0,0 +1,15 @@ |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
4 |
+let name2pairs acc (name, th) = |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
5 |
+ let acc = |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
6 |
+ if is_conj (concl th) then |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
7 |
+ let fold_fun (no, acc) th = (no + 1, (name ^ "_conjunct" ^ (string_of_int no), th) :: acc) in |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
8 |
+ snd (List.fold_left fold_fun (0, acc) (CONJUNCTS th)) |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
9 |
+ else acc |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
10 |
+ in (name, th) :: acc |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
11 |
+;; |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
12 |
+let dump_theorems () = |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
13 |
+ let oc = open_out "theorems" in |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
14 |
+ let all_thms = List.fold_left name2pairs [] !theorems in |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
15 |
+ output_value oc (map (fun (a,b) -> (a, dest_thm b)) all_thms); |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
16 |
+ close_out oc |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
17 |
+;; |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
18 |
+dump_theorems ();; |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
19 |
--- hol-light/stage1.ml 1970-01-01 01:00:00.000000000 +0100 |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
20 |
+++ hol-light-patched/stage1.ml 2025-01-18 11:12:11.185279392 +0100 |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
21 |
@@ -0,0 +1,4 @@ |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
22 |
+#use "hol.ml";; |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
23 |
+#use "update_database.ml";; |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
24 |
+#use "statements.ml";; |
|
02e107686442
move material from https://gitlab.inria.fr/hol-light-isabelle/hol-light 72b2b702eadb and https://gitlab.inria.fr/hol-light-isabelle/import ce58755b0232 into Isabelle repository: results from running "isabelle component_hol_light_import" of previous version;
wenzelm
parents:
diff
changeset
|
25 |
+exit 0;; |