1.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy	Mon Mar 26 16:27:43 2018 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy	Sat Mar 31 10:30:17 2018 +0200
     1.3 @@ -8,6 +8,22 @@
     1.4  
     1.5  ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
     1.6  
     1.7 +partial_function (tailrec)
     1.8 +  solve_equation :: "bool \<Rightarrow> real \<Rightarrow> bool list "
     1.9 +where
    1.10 +  "solve_equation eq bdv = [eq, eq, eq]"
    1.11 +ML {*
    1.12 +@{term solve_equation}
    1.13 +*}
    1.14 +
    1.15 +thm "solve_equation.simps"
    1.16 +ML {*
    1.17 +val thm = @{thm solve_equation.simps}
    1.18 +*} ML {*
    1.19 +Thm.prop_of thm
    1.20 +*} ML {*
    1.21 +*}
    1.22 +
    1.23  ML {*
    1.24  *} ML {*
    1.25  *}

     2.1 --- a/src/Tools/isac/ROOT	Mon Mar 26 16:27:43 2018 +0200
     2.2 +++ b/src/Tools/isac/ROOT	Sat Mar 31 10:30:17 2018 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      Author: Walther Neuper, TU Graz, 130715
     2.5     (c) due to copyright terms
     2.6  
     2.7 -$ export ISABELLE_VERSION=2015 # for libisabelle
     2.8 +$ export ISABELLE_VERSION=2017 # for libisabelle
     2.9  $ cd /usr/local/isabisac/
    2.10  $ ./bin/isabelle build -v -b Isac
    2.11  $ ./bin/isabelle build -v -b libisabelle_Isac
    2.12 @@ -12,6 +12,8 @@
    2.13  before out-outcommenting (*, browser_info = true*) below and ...
    2.14  $ ./bin/isabelle build -o browser_info -v -c HOL
    2.15  $ ./bin/isabelle build -o browser_info -v -b Isac
    2.16 +# this creates, among others:
    2.17 +# file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf
    2.18  *)
    2.19  
    2.20  session Isac in "~~/src/Tools/isac" = HOL +