test/Tools/isac/Test_Isac_Short.thy
changeset 60413 e997d57fbf7d
parent 60401 54d17d6d4245
child 60424 c3acf9c442ac
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Mon Sep 27 13:17:52 2021 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Mon Sep 27 20:24:24 2021 +0200
     1.3 @@ -175,6 +175,7 @@
     1.4  section \<open>test ML Code of isac\<close>
     1.5  subsection \<open>basic code first\<close>
     1.6    ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
     1.7 +  ML_file "BaseDefinitions/base-definitions.sml"
     1.8    ML_file "BaseDefinitions/libraryC.sml"
     1.9    ML_file "BaseDefinitions/rule-def.sml"
    1.10    ML_file "BaseDefinitions/eval-def.sml"
    1.11 @@ -293,18 +294,6 @@
    1.12    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
    1.13  (*ML_file "Knowledge/partial_fractions.sml"  hangs with ML_system_64 = "true"---Test_Isac_Short*)
    1.14    ML_file "Knowledge/polyeq-1.sml"
    1.15 -ML \<open>
    1.16 -\<close> ML \<open>                                                                
    1.17 -\<close> ML \<open>
    1.18 -\<close> ML \<open>
    1.19 -\<close> ML \<open>
    1.20 -\<close> ML \<open>
    1.21 -\<close> ML \<open>
    1.22 -\<close> ML \<open>
    1.23 -\<close> ML \<open>
    1.24 -\<close> ML \<open>
    1.25 -\<close> ML \<open>
    1.26 -\<close>
    1.27  (*ML_file "Knowledge/polyeq-2.sml"                                              Test_Isac_Short*)
    1.28  (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
    1.29    ML_file "Knowledge/calculus.sml"