# HG changeset patch
# User wenzelm
# Date 1565722448 -7200
# Node ID 1615b6808192a7c4b0e388b3f61b129d69272b2b
# Parent  7783bece74b440b4b19851150b878d4325dda640
NEWS and example for Theory.join_theory;

diff -r 7783bece74b4 -r 1615b6808192 NEWS
--- 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)
 -------------------------------
diff -r 7783bece74b4 -r 1615b6808192 src/HOL/ROOT
--- 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
diff -r 7783bece74b4 -r 1615b6808192 src/HOL/ex/Join_Theory.thy
--- /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