--- a/NEWS Tue Aug 13 20:19:15 2019 +0200
+++ b/NEWS Tue Aug 13 20:54:08 2019 +0200
@@ -34,6 +34,13 @@
associates to the left now as is customary.
+*** ML ***
+
+* Theory construction may be forked internally, the operation
+Theory.join_theory recovers a single result theory. See also the example
+in theory "HOL-ex.Join_Theory".
+
+
New in Isabelle2019 (June 2019)
-------------------------------
--- a/src/HOL/ROOT Tue Aug 13 20:19:15 2019 +0200
+++ b/src/HOL/ROOT Tue Aug 13 20:54:08 2019 +0200
@@ -593,6 +593,7 @@
Iff_Oracle
Induction_Schema
Intuitionistic
+ Join_Theory
Lagrange
List_to_Set_Comprehension_Examples
LocaleTest2
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Join_Theory.thy Tue Aug 13 20:54:08 2019 +0200
@@ -0,0 +1,47 @@
+(* Title: HOL/ex/Join_Theory.thy
+ Author: Makarius
+*)
+
+section \<open>Join theory content from independent (parallel) specifications\<close>
+
+theory Join_Theory
+ imports Main
+begin
+
+subsection \<open>Example template\<close>
+
+definition "test = True"
+lemma test: "test" by (simp add: test_def)
+
+
+subsection \<open>Specification as Isabelle/ML function\<close>
+
+ML \<open>
+ fun spec i lthy =
+ let
+ val b = Binding.name ("test" ^ string_of_int i)
+ val ((t, (_, def)), lthy') = lthy
+ |> Local_Theory.define ((b, NoSyn), ((Binding.empty, []), \<^term>\<open>True\<close>));
+ val th =
+ Goal.prove lthy' [] [] (HOLogic.mk_Trueprop t)
+ (fn {context = goal_ctxt, ...} => asm_full_simp_tac (goal_ctxt addsimps [def]) 1);
+ val (_, lthy'') = lthy' |> Local_Theory.note ((b, []), [th]);
+ in lthy'' end;
+\<close>
+
+
+subsection \<open>Example application\<close>
+
+setup \<open>
+ fn thy =>
+ let val forked_thys = Par_List.map (fn i => Named_Target.theory_map (spec i) thy) (1 upto 10)
+ in Theory.join_theory forked_thys end
+\<close>
+
+term test1
+thm test1
+
+term test10
+thm test10
+
+end