test/Tools/isac/Test_Isac.thy
changeset 59917 e98d714cca1a
parent 59914 ab5bd5c37e13
child 59919 3a7fb975af9d
equal deleted inserted replaced
59916:2c0c34b18050 59917:e98d714cca1a
   189   ML_file "BaseDefinitions/rule-set.sml"
   189   ML_file "BaseDefinitions/rule-set.sml"
   190   ML_file "BaseDefinitions/check-unique.sml"
   190   ML_file "BaseDefinitions/check-unique.sml"
   191 (*called by Know_Store*)
   191 (*called by Know_Store*)
   192   ML_file "BaseDefinitions/calcelems.sml"
   192   ML_file "BaseDefinitions/calcelems.sml"
   193   ML_file "BaseDefinitions/termC.sml"
   193   ML_file "BaseDefinitions/termC.sml"
   194   ML_file substitution.sml
   194   ML_file "BaseDefinitions/substitution.sml"
   195   ML_file "BaseDefinitions/contextC.sml"
   195   ML_file "BaseDefinitions/contextC.sml"
   196   ML_file "BaseDefinitions/environment.sml"
   196   ML_file "BaseDefinitions/environment.sml"
   197   ML_file "BaseDefinitions/kestore.sml"    (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
   197   ML_file "BaseDefinitions/kestore.sml"    (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
   198 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
   198 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
   199   ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
   199   ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)