1.1 --- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Sep 05 18:09:56 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Nov 21 12:32:54 2018 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    lin_isolate_add2:  "(a +   bdv = 0) = (  bdv = (-1)*a)" and
     1.5    lin_isolate_div:   "[|Not(b=0)|] ==> (b*bdv = c) = (bdv = c / b)"
     1.6  
     1.7 -ML {*
     1.8 +ML \<open>
     1.9  val thy = @{theory};
    1.10  
    1.11  val LinEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
    1.12 @@ -69,10 +69,10 @@
    1.13       Rule.Calc ("Atools.pow" ,eval_binop "#power_"),
    1.14       *)
    1.15      ];
    1.16 -*}
    1.17 -setup {* KEStore_Elems.add_rlss 
    1.18 -  [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))] *}
    1.19 -ML {*
    1.20 +\<close>
    1.21 +setup \<open>KEStore_Elems.add_rlss 
    1.22 +  [("LinEq_erls", (Context.theory_name @{theory}, LinEq_erls))]\<close>
    1.23 +ML \<open>
    1.24      
    1.25  val LinPoly_simplify = prep_rls'(
    1.26    Rule.Rls {id = "LinPoly_simplify", preconds = [], 
    1.27 @@ -92,10 +92,10 @@
    1.28  		Rule.Calc ("Atools.pow" ,eval_binop "#power_")
    1.29  		],
    1.30         scr = Rule.EmptyScr});
    1.31 -*}
    1.32 -setup {* KEStore_Elems.add_rlss 
    1.33 -  [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))] *}
    1.34 -ML {*
    1.35 +\<close>
    1.36 +setup \<open>KEStore_Elems.add_rlss 
    1.37 +  [("LinPoly_simplify", (Context.theory_name @{theory}, LinPoly_simplify))]\<close>
    1.38 +ML \<open>
    1.39  
    1.40  (*isolate the bound variable in an linear equation; 'bdv' is a meta-constant*)
    1.41  val LinEq_simplify = prep_rls'(
    1.42 @@ -113,13 +113,13 @@
    1.43  	      (*   bx=c -> x=c/b *)  
    1.44  	      ],
    1.45       scr = Rule.EmptyScr});
    1.46 -*}
    1.47 -setup {* KEStore_Elems.add_rlss 
    1.48 -  [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))] *}
    1.49 +\<close>
    1.50 +setup \<open>KEStore_Elems.add_rlss 
    1.51 +  [("LinEq_simplify", (Context.theory_name @{theory}, LinEq_simplify))]\<close>
    1.52  
    1.53  (*----------------------------- problem types --------------------------------*)
    1.54  (* ---------linear----------- *)
    1.55 -setup {* KEStore_Elems.add_pbts
    1.56 +setup \<open>KEStore_Elems.add_pbts
    1.57    [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Celem.e_pblID
    1.58        (["LINEAR", "univariate", "equation"],
    1.59          [("#Given" ,["equality e_e", "solveFor v_v"]),
    1.60 @@ -129,10 +129,10 @@
    1.61                "((lhs e_e) has_degree_in v_v)=1",
    1.62  	            "((rhs e_e) has_degree_in v_v)=1"]),
    1.63            ("#Find"  ,["solutions v_v'i'"])],
    1.64 -        LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))] *}
    1.65 +        LinEq_prls, SOME "solve (e_e::bool, v_v)", [["LinEq", "solve_lineq_equation"]]))]\<close>
    1.66  
    1.67  (*-------------- methods------------------------------------------------------*)
    1.68 -setup {* KEStore_Elems.add_mets
    1.69 +setup \<open>KEStore_Elems.add_mets
    1.70    [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
    1.71        (["LinEq"], [],
    1.72          {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule.e_rls, prls = Rule.e_rls,
    1.73 @@ -157,8 +157,8 @@
    1.74            "                                     LinEq_simplify True)) @@  " ^
    1.75            "            (Repeat(Try (Rewrite_Set LinPoly_simplify     False)))) e_e " ^
    1.76            " in ((Or_to_List e_e)::bool list))")]
    1.77 -*}
    1.78 -ML {* Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"]; *}
    1.79 +\<close>
    1.80 +ML \<open>Specify.get_met' @{theory} ["LinEq","solve_lineq_equation"];\<close>
    1.81  
    1.82  end
    1.83