1.1 --- a/src/Tools/isac/Knowledge/Biegelinie.thy Wed Apr 04 12:41:03 2018 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Biegelinie.thy Wed Apr 11 14:44:46 2018 +0200
1.3 @@ -184,6 +184,10 @@
1.4 scr = Rule.EmptyScr};
1.5 *}
1.6
1.7 +section \<open>Methods\<close>
1.8 +
1.9 +subsection \<open>Sub-problem "integrate and determine constants", little modularisation\<close>
1.10 +
1.11 setup {* KEStore_Elems.add_mets
1.12 [Specify.prep_met @{theory} "met_biege" [] Celem.e_metID
1.13 (["IntegrierenUndKonstanteBestimmen"],
1.14 @@ -260,13 +264,43 @@
1.15 " B__B = Take B__B; " ^
1.16 " B__B = ((Substitute c_1_2) @@ " ^
1.17 " (Rewrite_Set_Inst [(bdv, x)] make_ratpoly_in False)) B__B " ^
1.18 - " in B__B)"),
1.19 - Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
1.20 + " in B__B)")]
1.21 +*}
1.22 +subsection \<open>Sub-problem "integrate and determine constants", nicely modularised\<close>
1.23 +(*------------------------------------------------------------------------------------\\\
1.24 +consts
1.25 + Biegelinie' :: ID vonBelastungZu :: ID Biegelinien :: ID ausBelastung :: ID
1.26 + setzeRandbedingungen :: ID setzeRandbedingungenEin :: ID LINEAR :: ID system :: ID
1.27 + no_met :: ID make_ratpoly_in :: ID
1.28 + bdv :: real c :: real c_2 :: real c_3 :: real c_4 :: real
1.29 +
1.30 +partial_function (tailrec) biegelinie ::
1.31 + "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> (real \<Rightarrow> real) \<Rightarrow> bool list \<Rightarrow> bool"
1.32 +where
1.33 + "biegelinie l q v b s =
1.34 + (let
1.35 + funs = (SubProblem (Biegelinie',
1.36 + [vonBelastungZu, Biegelinien], [Biegelinien, ausBelastung])
1.37 + [REAL q, REAL v]);
1.38 + equs = (SubProblem (Biegelinie',
1.39 + [setzeRandbedingungen, Biegelinien], [Biegelinien, setzeRandbedingungenEin])
1.40 + [BOOL_LIST funs, BOOL_LIST s]);
1.41 + cons = (SubProblem (Biegelinie', [LINEAR, system], [no_met])
1.42 + [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]);
1.43 + B = Take (lastI funs);
1.44 + B = ((Substitute cons) @@
1.45 + (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B
1.46 + in B) "
1.47 +
1.48 + \\\------------------------------------------------------------------------------------*)
1.49 +
1.50 +setup {* KEStore_Elems.add_mets
1.51 + [Specify.prep_met @{theory} "met_biege_2" [] Celem.e_metID
1.52 (["IntegrierenUndKonstanteBestimmen2"],
1.53 - [("#Given" ,["Traegerlaenge l_l", "Streckenlast q__q", "FunktionsVariable v_v"]),
1.54 - (*("#Where",["0 < l_l"]), ...wait for < and handling Arbfix*)
1.55 - ("#Find" ,["Biegelinie b_b"]),
1.56 - ("#Relate",["Randbedingungen r_b"])],
1.57 + [("#Given" ,["Traegerlaenge l", "Streckenlast q", "FunktionsVariable v"]),
1.58 + (*("#Where",["0 < l"]), ...wait for < and handling Arbfix*)
1.59 + ("#Find" ,["Biegelinie b"]),
1.60 + ("#Relate",["Randbedingungen s"])],
1.61 {rew_ord'="tless_true",
1.62 rls' = Rule.append_rls "erls_IntegrierenUndK.." Rule.e_rls
1.63 [Rule.Calc ("Atools.ident",eval_ident "#ident_"),
1.64 @@ -280,24 +314,22 @@
1.65 Rule.Thm ("if_True",TermC.num_str @{thm if_True}),
1.66 Rule.Thm ("if_False",TermC.num_str @{thm if_False})],
1.67 prls = Rule.Erls, crls = Atools_erls, errpats = [], nrls = Rule.Erls},
1.68 - "Script Biegelinie2Script " ^
1.69 - "(l_l::real) (q__q::real) (v_v::real) (b_b::real=>real) (r_b::bool list) = " ^
1.70 - " (let " ^
1.71 - " (fun_s:: bool list) = " ^
1.72 - " (SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], " ^
1.73 - " [Biegelinien,ausBelastung]) " ^
1.74 - " [REAL q__q, REAL v_v]); " ^
1.75 - " (equ_s::bool list) = " ^
1.76 - " (SubProblem (Biegelinie',[setzeRandbedingungen,Biegelinien], " ^
1.77 - " [Biegelinien,setzeRandbedingungenEin]) " ^
1.78 - " [BOOL_LIST fun_s, BOOL_LIST r_b]); " ^
1.79 - " (con_s::bool list) = " ^
1.80 - " (SubProblem (Biegelinie',[LINEAR,system],[no_met]) " ^
1.81 - " [BOOL_LIST equ_s, REAL_LIST [c,c_2,c_3,c_4]]); " ^
1.82 - " B_B = Take (lastI fun_s); " ^
1.83 - " B_B = ((Substitute con_s) @@ " ^
1.84 - " (Rewrite_Set_Inst [(bdv, v_v)] make_ratpoly_in False)) B_B " ^
1.85 - " in B_B)"),
1.86 + "Script Biegelinie2Script " ^
1.87 + "(l::real) (q :: real) (v :: real) (b :: real => real) (s :: bool list) = " ^
1.88 + " (let " ^
1.89 + " (funs :: bool list) = (SubProblem (Biegelinie', " ^
1.90 + " [vonBelastungZu, Biegelinien], [Biegelinien, ausBelastung]) " ^
1.91 + " [REAL q, REAL v]); " ^
1.92 + " (equs :: bool list) = (SubProblem (Biegelinie', " ^
1.93 + " [setzeRandbedingungen, Biegelinien], [Biegelinien, setzeRandbedingungenEin]) " ^
1.94 + " [BOOL_LIST funs, BOOL_LIST s]); " ^
1.95 + " (cons :: bool list) = (SubProblem (Biegelinie', " ^
1.96 + " [LINEAR, system], [no_met]) " ^
1.97 + " [BOOL_LIST equs, REAL_LIST [c, c_2, c_3, c_4]]); " ^
1.98 + " B = Take (lastI funs); " ^
1.99 + " B = ((Substitute cons) @@ " ^
1.100 + " (Rewrite_Set_Inst [(bdv, v)] make_ratpoly_in False)) B " ^
1.101 + " in B) "),
1.102 Specify.prep_met @{theory} "met_biege_intconst_2" [] Celem.e_metID
1.103 (["IntegrierenUndKonstanteBestimmen","2xIntegrieren"], [],
1.104 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.105 @@ -317,8 +349,12 @@
1.106 (["Biegelinien"], [],
1.107 {rew_ord'="tless_true", rls'=Rule.Erls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, crls = Atools_erls,
1.108 errpats = [], nrls = Rule.e_rls},
1.109 - "empty_script"),
1.110 - Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
1.111 + "empty_script")]
1.112 +*}
1.113 +subsection \<open>Compute the general bending line\<close>
1.114 +
1.115 +setup {* KEStore_Elems.add_mets
1.116 + [Specify.prep_met @{theory} "met_biege_ausbelast" [] Celem.e_metID
1.117 (["Biegelinien", "ausBelastung"],
1.118 [("#Given" ,["Streckenlast q__q", "FunktionsVariable v_v"]),
1.119 ("#Find" ,["Funktionen fun_s"])],
1.120 @@ -354,8 +390,12 @@
1.121 " (SubProblem (Biegelinie',[named,integrate,function], " ^
1.122 " [diff,integration,named]) " ^
1.123 " [REAL (rhs N__N), REAL v_v, REAL_REAL y]) " ^
1.124 - " in [Q__Q, M__M, N__N, B__B])"),
1.125 - Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
1.126 + " in [Q__Q, M__M, N__N, B__B])")]
1.127 +*}
1.128 +subsection \<open>Substitute the constraints into the equations\<close>
1.129 +
1.130 +setup {* KEStore_Elems.add_mets
1.131 + [Specify.prep_met @{theory} "met_biege_setzrand" [] Celem.e_metID
1.132 (["Biegelinien", "setzeRandbedingungenEin"],
1.133 [("#Given" , ["Funktionen fun_s", "Randbedingungen r_b"]),
1.134 ("#Find" , ["Gleichungen equs'''"])],
1.135 @@ -413,8 +453,12 @@
1.136 " (SubProblem (Biegelinie',[makeFunctionTo,equation]," ^
1.137 " [Equation,fromFunction]) " ^
1.138 " [BOOL (hd f_s), BOOL b_4]) " ^
1.139 - " in [e_1,e_2,e_3,e_4])"*)),
1.140 - Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
1.141 + " in [e_1,e_2,e_3,e_4])"*))]
1.142 +*}
1.143 +subsection \<open>Transform an equality into a function\<close>
1.144 +
1.145 +setup {* KEStore_Elems.add_mets
1.146 + [Specify.prep_met @{theory} "met_equ_fromfun" [] Celem.e_metID
1.147 (["Equation","fromFunction"],
1.148 [("#Given" ,["functionEq fu_n","substitution su_b"]),
1.149 ("#Find" ,["equality equ'''"])],
2.1 --- a/src/Tools/isac/Knowledge/Poly.thy Wed Apr 04 12:41:03 2018 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Wed Apr 11 14:44:46 2018 +0200
2.3 @@ -914,6 +914,7 @@
2.4 Rule.Thm ("sym_add_assoc",
2.5 TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
2.6
2.7 +(* probably perfectly replaced by auto-generated version *)
2.8 val scr_make_polynomial =
2.9 "Script Expand_binoms t_t = " ^
2.10 "(Repeat " ^
2.11 @@ -968,6 +969,7 @@
2.12 scr = Rule.EmptyScr
2.13 }); *)
2.14
2.15 +(* replacement by auto-generated version seemed to cause ERROR in algein.sml *)
2.16 val scr_expand_binoms =
2.17 "Script Expand_binoms t_t =" ^
2.18 "(Repeat " ^
2.19 @@ -1605,7 +1607,16 @@
2.20 Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
2.21 SOME "Simplify t_t",
2.22 [["simplification","for_polynomials"]]))] *}
2.23 +
2.24 (** methods **)
2.25 +(*-----
2.26 +consts
2.27 + norm_Poly :: ID
2.28 +partial_function (tailrec) simplify :: "real \<Rightarrow> real"
2.29 + where
2.30 + "simplify term = ((Rewrite_Set norm_Poly False) term)"
2.31 +
2.32 +-----*)
2.33 setup {* KEStore_Elems.add_mets
2.34 [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
2.35 (["simplification","for_polynomials"],
2.36 @@ -1621,4 +1632,7 @@
2.37 " ((Rewrite_Set norm_Poly False) t_t)")]
2.38 *}
2.39
2.40 +ML {*
2.41 +*} ML {*
2.42 +*}
2.43 end
3.1 --- a/src/Tools/isac/ProgLang/Atools.thy Wed Apr 04 12:41:03 2018 +0200
3.2 +++ b/src/Tools/isac/ProgLang/Atools.thy Wed Apr 11 14:44:46 2018 +0200
3.3 @@ -41,6 +41,7 @@
3.4 filter'_sameFunId:: "[real, bool list] => bool list"
3.5 ("filter'_sameFunId _ _" 10)
3.6 boollist2sum :: "bool list => real"
3.7 + lastI :: "'a list \<Rightarrow> 'a"
3.8
3.9 axiomatization where (*for evaluating the assumptions of conditional rules*)
3.10
4.1 --- a/src/Tools/isac/calcelems.sml Wed Apr 04 12:41:03 2018 +0200
4.2 +++ b/src/Tools/isac/calcelems.sml Wed Apr 11 14:44:46 2018 +0200
4.3 @@ -598,28 +598,27 @@
4.4
4.5 (* data for methods stored in 'methods'-database*)
4.6 type met =
4.7 - {guh : guh, (*unique within this isac-knowledge *)
4.8 - mathauthors: string list, (*copyright *)
4.9 - init : pblID, (*WN060721 introduced mistakenly--TODO.REMOVE!*)
4.10 - rew_ord' : Rule.rew_ord', (*for rules in Detail
4.11 - TODO.WN0509 store fun itself, see 'type pbt'*)
4.12 - erls : Rule.rls, (*the eval_rls for cond. in rules FIXME "rls'
4.13 - instead erls in "fun prep_met" *)
4.14 - srls : Rule.rls, (*for evaluating list expressions in scr *)
4.15 - prls : Rule.rls, (*for evaluating predicates in modelpattern *)
4.16 - crls : Rule.rls, (*for check_elementwise, ie. formulae in calc.*)
4.17 - nrls : Rule.rls, (*canonical simplifier specific for this met *)
4.18 - errpats : Rule.errpat list,(*error patterns expected in this method *)
4.19 - calc : Rule.calc list, (*Theory_Data in fun prep_met *)
4.20 - (*branch : TransitiveB set in append_problem at generation ob pblobj
4.21 - FIXXXME.0308: set branch from met in Apply_Method ? *)
4.22 - ppc : pat list, (*.items in given, find, relate;
4.23 + {guh : guh, (* unique within this isac-knowledge *)
4.24 + mathauthors: string list, (* copyright *)
4.25 + init : pblID, (* WN060721 introduced mistakenly--TODO.REMOVE! *)
4.26 + rew_ord' : Rule.rew_ord', (* for rules in Detail
4.27 + TODO.WN0509 store fun itself, see 'type pbt' *)
4.28 + erls : Rule.rls, (* the eval_rls for cond. in rules FIXME "rls'
4.29 + instead erls in "fun prep_met" *)
4.30 + srls : Rule.rls, (* for evaluating list expressions in scr *)
4.31 + prls : Rule.rls, (* for evaluating predicates in modelpattern *)
4.32 + crls : Rule.rls, (* for check_elementwise, ie. formulae in calc. *)
4.33 + nrls : Rule.rls, (* canonical simplifier specific for this met *)
4.34 + errpats : Rule.errpat list,(* error patterns expected in this method *)
4.35 + calc : Rule.calc list, (* Theory_Data in fun prep_met *)
4.36 + (*branch : TransitiveB set in append_problem at generation ob pblobj *)
4.37 + ppc : pat list, (* items in given, find, relate;
4.38 items (in "#Find") which need not occur in the arg-list of a SubProblem
4.39 are 'copy-named' with an identifier "*'.'".
4.40 copy-named items are 'generating' if they are NOT "*'''" ?WN120516??
4.41 - see ME/calchead.sml 'fun is_copy_named'. *)
4.42 - pre : term list, (*preconditions in where *)
4.43 - scr : Rule.scr (*prep_met gets progam or string "empty_script" *)
4.44 + see ME/calchead.sml 'fun is_copy_named'. *)
4.45 + pre : term list, (* preconditions in where *)
4.46 + scr : Rule.scr (* prep_met gets progam or string "empty_script" *)
4.47 };
4.48 val e_met = {guh = "met_empty", mathauthors = [], init = e_metID, rew_ord' = "e_rew_ord'",
4.49 erls = Rule.e_rls, srls = Rule.e_rls, prls = Rule.e_rls, calc = [], crls = Rule.e_rls,
5.1 --- a/test/Tools/isac/Test_Isac.thy Wed Apr 04 12:41:03 2018 +0200
5.2 +++ b/test/Tools/isac/Test_Isac.thy Wed Apr 11 14:44:46 2018 +0200
5.3 @@ -183,113 +183,7 @@
5.4 ML_file "xmlsrc/datatypes.sml" (*TODO/part.*)
5.5 ML_file "xmlsrc/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)
5.6 ML_file "xmlsrc/thy-hierarchy.sml"
5.7 -
5.8 -ML {*
5.9 -"~~~~~ fun xxx, args:"; val () = ();
5.10 -*} ML {*
5.11 -"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
5.12 -"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
5.13 -"----------- gen.minimal KEStore_Elems from Test_Build_Thydata.thy";
5.14 - val isacrlsthms = KEStore_Elems.get_rlss @{theory Test_Build_Thydata}
5.15 -(* CHANGE FOR CODE ^^^^^^^^^^^^^^^^^^^^^^^^^^^*)
5.16 - |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "list_rls" (*unpleasant in test*)
5.17 - |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rrls" (*unpleasant in test*)
5.18 - |> remove (fn (rlsID, (rls', (_, _))) => rlsID = rls') "e_rls" (*unpleasant in test*)
5.19 - |> thms_of_rlss @{theory} (*length = 4*)
5.20 -
5.21 - val rlsthmsNOTisac = isacrlsthms (*length = 2*)
5.22 - |> filter (fn (deriv, _) =>
5.23 - member op= (map Context.theory_name isabthys') (thyID_of_derivation_name deriv))
5.24 -;
5.25 -val (knowthys', progthys') = ([@{theory Test_Build_Thydata}], [@{theory Test_Build_Thydata}])
5.26 -;
5.27 -val thydata_list =
5.28 - collect_part "IsacKnowledge" knowledge_parent knowthys' @
5.29 - (map (collect_isab "Isabelle") rlsthmsNOTisac) @
5.30 - collect_part "IsacScripts" proglang_parent progthys' (* only the thms, no rls *)
5.31 -;
5.32 -*} ML {*
5.33 -thydata_list
5.34 -(*
5.35 - [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
5.36 - Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
5.37 - mathauthors = ["isac-team"], thm = "?thm111.0 = ?thm111.0 + 111"}),
5.38 - (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
5.39 - Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
5.40 - mathauthors = ["isac-team"], thm = "?thm222.0 = ?thm222.0 + 222"}),
5.41 - (["Isabelle", "HOL", "Theorems", "refl"],
5.42 - Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl", mathauthors =
5.43 - ["Isabelle team, TU Munich"], thm = "?t = ?t"}),
5.44 - (["Isabelle", "Fun", "Theorems", "o_def"],
5.45 - Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_Fun-thm-o_def", mathauthors =
5.46 - ["Isabelle team, TU Munich"], thm = "?f \<circ> ?g = (\<lambda>x. ?f (?g x))"}),
5.47 - (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
5.48 - Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
5.49 - mathauthors = ["isac-team"], thm = "?thm111.0 = ?thm111.0 + 111"}),
5.50 - (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
5.51 - Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
5.52 - mathauthors = ["isac-team"], thm = "?thm222.0 = ?thm222.0 + 222"})]
5.53 -*)
5.54 -*} ML {*
5.55 -*} ML {*
5.56 -case thydata_list of (*length = 8*)
5.57 - [(["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm111"],
5.58 - Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm111",
5.59 - mathauthors = ["isac-team"], thm = _}),
5.60 - (["IsacKnowledge", "Test_Build_Thydata", "Theorems", "thm222"],
5.61 - Hthm {coursedesign = [], fillpats = [], guh = "thy_isac_Test_Build_Thydata-thm-thm222",
5.62 - mathauthors = ["isac-team"], thm = _}),
5.63 - (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls111"],
5.64 - Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls111",
5.65 - mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
5.66 - (["IsacKnowledge", "Test_Build_Thydata", "Rulesets", "rls222"],
5.67 - Hrls {coursedesign = [], guh = "thy_isac_Test_Build_Thydata-rls-rls222",
5.68 - mathauthors = ["isac-team"], thy_rls = ("Test_Build_Thydata", Rls _)}),
5.69 - (["Isabelle", "HOL", "Theorems", "refl"],
5.70 - Hthm {coursedesign = [], fillpats = [], guh = "thy_isab_HOL-thm-refl",
5.71 - mathauthors = ["Isabelle team, TU Munich"], thm = _}),
5.72 - (["Isabelle", "Fun", "Theorems", "o_def"], Hthm {coursedesign = [], fillpats = [],
5.73 - guh = "thy_isab_Fun-thm-o_def", mathauthors = ["Isabelle team, TU Munich"], thm = _}),
5.74 - (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm111"],
5.75 - Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm111",
5.76 - mathauthors = ["isac-team"], thm = _}),
5.77 - (["IsacScripts", "Test_Build_Thydata", "Theorems", "thm222"],
5.78 - Hthm {coursedesign = [], fillpats = [], guh = "thy_scri_Test_Build_Thydata-thm-thm222",
5.79 - mathauthors = ["isac-team"], thm = _})] => ()
5.80 -| _ => error "collect thydata from Test_Build_Thydata changed";
5.81 -;
5.82 -(* we store locally on MINIthehier instead on KEStore, see KEStore: *)
5.83 - fun add_the (thydata, theID) = add_thydata ([], theID) thydata;
5.84 -val thes = map (fn (a, b) => (b, a)) thydata_list
5.85 -val MINIthehier = (fold add_the thes) (KEStore_Elems.get_thes @{theory Test_Build_Thydata});
5.86 -*} ML {*
5.87 -"~~~~~ fun xxx, args:"; val () = ();
5.88 -*} ML {*
5.89 -*} ML {*
5.90 -*} ML {*
5.91 -*} ML {*
5.92 -*} ML {*
5.93 -*} ML {*
5.94 -*} ML {*
5.95 -*} ML {*
5.96 -*} ML {*
5.97 -*} ML {*
5.98 -*} ML {*
5.99 -*} ML {*
5.100 -*} ML {*
5.101 -*} ML {*
5.102 -*} ML {*
5.103 -"~~~~~ fun xxx, args:"; val () = ();
5.104 -*}
5.105 -
5.106 -
5.107 -
5.108 -
5.109 -
5.110 -
5.111 -
5.112 -
5.113 -ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
5.114 + ML_file "xmlsrc/interface-xml.sml" (*TODO after 2009-2*)
5.115 ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
5.116 ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
5.117 ML_file "Frontend/messages.sml"
6.1 --- a/ztest-to-coding.sh Wed Apr 04 12:41:03 2018 +0200
6.2 +++ b/ztest-to-coding.sh Wed Apr 11 14:44:46 2018 +0200
6.3 @@ -7,5 +7,5 @@
6.4 cd ../../../ # go back to ~~/.
6.5
6.6 # immediately go to correcting code in Interpret/
6.7 -#./bin/isabelle jedit src/Tools/isac/ProgLang/ProgLang.thy &
6.8 -./bin/isabelle jedit src/Tools/isac/Isac_Protocol.thy &
6.9 +./bin/isabelle jedit src/Tools/isac/Knowledge/Biegelinie.thy &
6.10 +#./bin/isabelle jedit src/Tools/isac/Isac_Protocol.thy &