1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Nov 14 15:51:10 2016 +0100
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Thu Nov 17 16:40:27 2016 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:  build and test isac on Isabelle2014
     1.5 +(*  Title:  build and test isac
     1.6      Author: Walther Neuper, TU Graz, 100808
     1.7     (c) due to copyright terms
     1.8  

     2.1 --- a/src/Tools/isac/Interpret/script.sml	Mon Nov 14 15:51:10 2016 +0100
     2.2 +++ b/src/Tools/isac/Interpret/script.sml	Thu Nov 17 16:40:27 2016 +0100
     2.3 @@ -27,7 +27,7 @@
     2.4    val rule2thm'' : rule -> thm''
     2.5    val rule2rls' : rule -> string
     2.6  
     2.7 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\*)
     2.8 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
     2.9    datatype asap = Aundef | AssOnly | AssGen
    2.10    datatype appy_ = Napp_ | Skip_
    2.11    val itms2args : 'a -> metID -> itm list -> term list
    2.12 @@ -43,14 +43,14 @@
    2.13    val nstep_up : theory' * rls -> ptree * pos' -> scr -> env -> lrd list -> appy_ -> 
    2.14      term option -> term -> appy
    2.15    val upd_env_opt : env -> term option * term -> env
    2.16 -(*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.17 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    2.18  end 
    2.19  
    2.20  (* traces the leaves (ie. non-tactical nodes) of Prog found by next_tac, see "and scr" *)   
    2.21  val trace_script = Unsynchronized.ref false; (* TODO: how are traces done in Isabelle? *)
    2.22  
    2.23  (**)
    2.24 -structure Lucin(*: LUCAS_INTERPRETER*) =
    2.25 +structure Lucin: LUCAS_INTERPRETER(**) =
    2.26  struct
    2.27  (**)
    2.28  (* data for creating a new node in ctree; designed for use as:

     3.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Nov 14 15:51:10 2016 +0100
     3.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Nov 17 16:40:27 2016 +0100
     3.3 @@ -19,13 +19,14 @@
     3.4  not declared in the signatures.
     3.5  
     3.6  In order to maintain these tests without changes, this has to be done before running tests:
     3.7 -* Query replace in src/Tools/isac:
     3.8 +(1) Query replace in src/Tools/isac:
     3.9      "--- ! aktivate for Test_Isac BEGIN ---\* )" --> "--- ! aktivate for Test_Isac BEGIN ---\*)"
    3.10      "( *\--- ! aktivate for Test_Isac END ---"   --> "(*\--- ! aktivate for Test_Isac END ---"
    3.11    This extends the signatures with some functions required for some tests.
    3.12 -* The same query replace below; this opens all structures.
    3.13  
    3.14 -*********************** DON'T FORGET TO REVERSE THESE CHANGES AFTER TESTS ***********************
    3.15 +Running Test_Isac.thy opens all structures, see code after "begin" below.
    3.16 +
    3.17 +*********************** DON'T FORGET TO REVERSE CHANGE (1) AFTER TESTS ***********************
    3.18  \<close>
    3.19  
    3.20  section \<open>Run the tests\<close>