1.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Dec 09 14:22:24 2020 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Dec 09 14:37:10 2020 +0100
     1.3 @@ -128,7 +128,9 @@
     1.4    open Solve;                  (* NONE *)
     1.5    open ContextC;               transfer_asms_from_to;
     1.6    open Tactic;                 (* NONE *)
     1.7 -  open P_Model;                  (* NONE *)
     1.8 +  open I_Model;
     1.9 +  open O_Model;
    1.10 +  open P_Model;                (* NONE *)
    1.11    open Rewrite;
    1.12    open Eval;                   get_pair;
    1.13    open TermC;                  atomt;
    1.14 @@ -142,19 +144,51 @@
    1.15    open UnparseC
    1.16  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.17  \<close>
    1.18 +ML_file "BaseDefinitions/libraryC.sml"
    1.19  
    1.20 +section \<open>code for copy & paste ===============================================================\<close>
    1.21  ML \<open>
    1.22  "~~~~~ fun xxx , args:"; val () = ();
    1.23  "~~~~~ and xxx , args:"; val () = ();
    1.24 -"~~~~~ from fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
    1.25 +"~~~~~ fun xxx \<longrightarrow>fun yyy \<longrightarrow>fun zzz , return:"; val () = ();
    1.26  (*if*) (*then*); (*else*);   (*case*) (*of*);  (*return from xxx*);
    1.27  "xx"
    1.28  ^ "xxx"   (*+*) (*!for return!*) (*isa*) (*REP*) (**)
    1.29 +(*/------------------- step into XXXXX -----------------------------------------------------\*)
    1.30 +(*-------------------- stop step into XXXXX -------------------------------------------------*)
    1.31 +(*\------------------- step into XXXXX -----------------------------------------------------/*)
    1.32 +(*-------------------- contiue step into XXXXX ----------------------------------------------*)
    1.33 +(*/------------------- check entry to XXXXX ------------------------------------------------\*)
    1.34 +(*\------------------- check entry to XXXXX ------------------------------------------------/*)
    1.35 +(*/------------------- check within XXXXX --------------------------------------------------\*)
    1.36 +(*\------------------- check within XXXXX --------------------------------------------------/*)
    1.37 +(*/------------------- check result of XXXXX -----------------------------------------------\*)
    1.38 +(*\------------------- check result of XXXXX -----------------------------------------------/*)
    1.39 +(* final test ...*)
    1.40 +(*/------------------- build new fun XXXXX -------------------------------------------------\*)
    1.41 +(*\------------------- build new fun XXXXX -------------------------------------------------/*)
    1.42  \<close> ML \<open>
    1.43  \<close>
    1.44  ML \<open>
    1.45  \<close> ML \<open>
    1.46  \<close> ML \<open>
    1.47 +\<close>
    1.48 +text \<open>
    1.49 +  declare [[show_types]] 
    1.50 +  declare [[show_sorts]]            
    1.51 +  find_theorems "?a <= ?a"
    1.52 +  
    1.53 +  print_theorems
    1.54 +  print_facts
    1.55 +  print_statement ""
    1.56 +  print_theory
    1.57 +  ML_command \<open>Pretty.writeln prt\<close>
    1.58 +  declare [[ML_print_depth = 999]]
    1.59 +  declare [[ML_exception_trace]]
    1.60 +\<close>
    1.61 +
    1.62 +section \<open>===================================================================================\<close>
    1.63 +ML \<open>
    1.64  \<close> ML \<open>
    1.65  \<close> ML \<open>
    1.66  \<close> ML \<open>