(* Title: HOL/ex/Join_Theory.thy Author: Makarius \<open>Join theory content from independent (parallel) specifications\<close> theory Join_Theoryimports Mainbegin \<open>Example template\<close> definition "test = True" lemma test: "test" by (simp add: test_def)\<open>Specification as Isabelle/ML function\<close> \<open> fun spec i lthy =let "test" ^ string_of_int i)def )), lthy') = lthy \<^term>\<open>True\<close>)); ' [] [] (HOLogic.mk_Trueprop t) context = goal_ctxt, ...} => asm_full_simp_tac (goal_ctxt addsimps [def ]) 1);'' ) = lthy' |> Local_Theory.note ((b, []), [th]); in lthy'' end ;\<close> \<open>Example application\<close> setup \<open> let val forked_thys = Par_List.map (fn i => Named_Target.theory_map (spec i) thy) (1 upto 10)in Context .join_thys forked_thys end \<close> term test1thm test1term test10thm test10end quality 100%
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
