1.1 --- a/ROOTS	Thu Sep 24 13:11:51 2020 +0200
     1.2 +++ b/ROOTS	Thu Sep 24 15:48:52 2020 +0200
     1.3 @@ -10,5 +10,3 @@
     1.4  src/Sequents
     1.5  src/Doc
     1.6  src/Tools
     1.7 -src/Tools/isac
     1.8 -test/Tools/isac/ADDTESTS/session-get_theory/

     2.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml	Thu Sep 24 13:11:51 2020 +0200
     2.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml	Thu Sep 24 15:48:52 2020 +0200
     2.3 @@ -100,14 +100,14 @@
     2.4  fun sym_thm thm =
     2.5    let 
     2.6      val (derivation,
     2.7 -      {cert = cert, tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = tpairs, 
     2.8 -      prop = prop}) = Thm.rep_thm_G thm
     2.9 +      {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints, shyps = shyps,
    2.10 +        hyps = hyps, tpairs = tpairs, prop = prop}) = Thm.rep_thm_G thm
    2.11      val (lhs, rhs) = (TermC.dest_equals o TermC.strip_trueprop o Logic.strip_imp_concl) prop
    2.12      val prop' = case TermC.strip_imp_prems' prop of
    2.13          NONE => HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs))
    2.14        | SOME cs => TermC.ins_concl cs (HOLogic.Trueprop $ (TermC.mk_equality (rhs, lhs)))
    2.15    in
    2.16 -    Thm.assbl_thm derivation cert tags maxidx shyps hyps tpairs prop'
    2.17 +    Thm.assbl_thm derivation cert tags maxidx constraints shyps hyps tpairs prop'
    2.18    end
    2.19  
    2.20  fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty

     3.1 --- a/src/Tools/isac/ROOT	Thu Sep 24 13:11:51 2020 +0200
     3.2 +++ b/src/Tools/isac/ROOT	Thu Sep 24 15:48:52 2020 +0200
     3.3 @@ -11,8 +11,19 @@
     3.4  # file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
     3.5  *)
     3.6  
     3.7 +(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
     3.8 +session Interpret = HOL +
     3.9 +  description \<open>
    3.10 +    Session Isac restricted to code required for paper
    3.11 +    "Lucas-Interpretation on Isabelle’s Functions".
    3.12 +    A first step towards formally checked documentation.
    3.13 +  \<close>
    3.14 +  options [document = false (*, browser_info = true*)]
    3.15 +  theories
    3.16 +    "Interpret/Interpret"
    3.17 +
    3.18  (* run "./bin/isabelle build -v -b Isac" *)
    3.19 -session Isac in "~~/src/Tools/isac" = HOL +
    3.20 +session Isac = Interpret +
    3.21    description \<open>
    3.22      Isac core, prototype of a math-engine and knowledge 
    3.23      for a TP-based educational mathematics assistant.
    3.24 @@ -24,14 +35,3 @@
    3.25    options [document = false (*, browser_info = true*)]
    3.26    theories
    3.27      Build_Isac
    3.28 -
    3.29 -(* run "./bin/isabelle build -v -b Lucas_Interpreter" *)
    3.30 -session Interpret = HOL +
    3.31 -  description \<open>
    3.32 -    Session Isac restricted to code required for Lucas_Interpreter.
    3.33 -    "Lucas-Interpretation on Isabelle’s Functions"
    3.34 -    and meant as a first step towards documentation.
    3.35 -  \<close>
    3.36 -  options [document = false (*, browser_info = true*)]
    3.37 -  theories
    3.38 -    "Interpret/Interpret"