1.1 --- a/src/Tools/isac/ROOT	Fri Aug 24 14:23:13 2018 +0200
     1.2 +++ b/src/Tools/isac/ROOT	Mon Aug 27 15:57:45 2018 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
     1.5  *)
     1.6  
     1.7 +(* run "./bin/isabelle build -v -b Isac" *)
     1.8  session Isac in "~~/src/Tools/isac" = HOL +
     1.9    description {*
    1.10      Isac core, prototype of a math-engine and knowledge 

     2.1 --- a/test/Tools/isac/ProgLang/calculate.sml	Fri Aug 24 14:23:13 2018 +0200
     2.2 +++ b/test/Tools/isac/ProgLang/calculate.sml	Mon Aug 27 15:57:45 2018 +0200
     2.3 @@ -306,7 +306,7 @@
     2.4  "----------- get_pair with 3 args --------------------------------";
     2.5  val (thy, op_, ef, arg) =
     2.6      (thy, "EqSystem.occur'_exactly'_in", 
     2.7 -     assoc_calc' (Thy_Info_get_theory "EqSystem") "occur_exactly_in" |> snd |> snd,
     2.8 +     assoc_calc' (@{theory "EqSystem"}) "occur_exactly_in" |> snd |> snd,
     2.9       str2term
    2.10        "[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) / 2"
    2.11        );

     3.1 --- a/test/Tools/isac/ProgLang/rewrite.sml	Fri Aug 24 14:23:13 2018 +0200
     3.2 +++ b/test/Tools/isac/ProgLang/rewrite.sml	Mon Aug 27 15:57:45 2018 +0200
     3.3 @@ -105,7 +105,7 @@
     3.4    handle _ => error "rewrite.sml diff.behav. in rew_sub";
     3.5  
     3.6  "----- ordered rewriting";
     3.7 -fun tord (_:subst) pp = Term_Ord.termless pp;
     3.8 +fun tord (_:subst) pp = LibraryC.termless pp;
     3.9  if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
    3.10  else error "rewrite.sml diff.behav. in ord.rewr.";
    3.11  

     4.1 --- a/test/Tools/isac/ProgLang/termC.sml	Fri Aug 24 14:23:13 2018 +0200
     4.2 +++ b/test/Tools/isac/ProgLang/termC.sml	Mon Aug 27 15:57:45 2018 +0200
     4.3 @@ -646,7 +646,7 @@
     4.4              (Const ("Groups.times_class.times", _) $ Var (("n", 0), _) $ Var (("k", 0), _))) $
     4.5            (Const ("Rings.divide_class.divide", _) $ Var (("m", 0), _) $ Var (("n", 0), _)))) = prop;
     4.6  val SOME t' = strip_imp_prems' t;
     4.7 -if  term2str t' = "op \<Longrightarrow> (?k \<noteq> 0)" then () else error "strip_imp_prems' changed";
     4.8 +if  term2str t' = "(\<Longrightarrow>) (?k \<noteq> 0)" then () else error "strip_imp_prems' changed";
     4.9  
    4.10  val thm = TermC.num_str @{thm frac_sym_conv};
    4.11  val prop = (#prop o Thm.rep_thm) thm;

     5.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Aug 24 14:23:13 2018 +0200
     5.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Aug 27 15:57:45 2018 +0200
     5.3 @@ -115,11 +115,11 @@
     5.4  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
     5.5  *}
     5.6  
     5.7 -ML {*
     5.8 +ML \<open>
     5.9  "~~~~~ fun xxx, args:"; val () = ();
    5.10 -*} ML {*
    5.11 -*} ML {*
    5.12 -*}
    5.13 +\<close> ML \<open>
    5.14 +\<close> ML \<open>
    5.15 +\<close>
    5.16  
    5.17  ML {*
    5.18    KEStore_Elems.set_ref_thy @{theory};

     6.1 --- a/ztest-to-coding.sh	Fri Aug 24 14:23:13 2018 +0200
     6.2 +++ b/ztest-to-coding.sh	Mon Aug 27 15:57:45 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/Knowledge/Biegelinie.thy &
     6.8 +./bin/isabelle jedit src/Tools/isac/Build_Isac.thy &
     6.9  #./bin/isabelle jedit src/Tools/isac/Isac_Protocol.thy &