test/Tools/isac/Test_Isac.thy
changeset 59858 a2c32a38327a
parent 59848 06a5cfe04223
child 59865 75a9d629ea53
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Apr 08 16:56:47 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Apr 09 11:21:53 2020 +0200
     1.3 @@ -97,7 +97,8 @@
     1.4    open Env;
     1.5    open LI;                     scan_dn;
     1.6    open Istate;
     1.7 -  open Error_Pattern;
     1.8 +  open Error_Fill_Pattern;
     1.9 +  open Error_Fill_Def;
    1.10    open In_Chead;
    1.11    open Rtools;                 trtas2str;
    1.12    open Chead;                  pt_extract;
    1.13 @@ -126,7 +127,12 @@
    1.14    open Num_Calc;                   get_pair;
    1.15    open TermC;                  atomt;
    1.16    open Celem;                  e_pbt;
    1.17 -  open Rule;                   string_of_thm;
    1.18 +  open Rule;
    1.19 +  open Rule_Set
    1.20 +  open Exec_Def
    1.21 +  open ThyC
    1.22 +  open ThmC
    1.23 +  open Rewrite_Ord
    1.24  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
    1.25  \<close>
    1.26  
    1.27 @@ -142,6 +148,14 @@
    1.28  ML \<open>
    1.29  \<close> ML \<open>
    1.30  \<close> ML \<open>
    1.31 +\<close> ML \<open>
    1.32 +\<close> ML \<open>
    1.33 +\<close> ML \<open>
    1.34 +\<close> ML \<open>
    1.35 +\<close> ML \<open>
    1.36 +\<close> ML \<open>
    1.37 +\<close> ML \<open>
    1.38 +\<close> ML \<open>
    1.39  \<close>
    1.40  
    1.41  ML \<open>