test/Tools/isac/Test_Isac.thy
changeset 52105 2786cc9704c8
parent 52102 cd5494eb08fd
child 52106 7f3760f39bdc
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Mon Sep 16 11:28:43 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Mon Sep 16 12:20:00 2013 +0200
     1.3 @@ -12,9 +12,9 @@
     1.4  $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
     1.5  *)
     1.6  
     1.7 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
     1.8 -(* !!!!! wait a minute until Isac and the theories below are loaded !!!!! *)
     1.9 -(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.10 +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.11 +(* !!!!! wait a minute until session Isac and the theories below are loaded !!!!! *)
    1.12 +(* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
    1.13  
    1.14  theory Test_Isac imports Isac
    1.15    "ADDTESTS/Ctxt"
    1.16 @@ -75,7 +75,7 @@
    1.17    ML_file "Interpret/inform.sml"
    1.18  (*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
    1.19    ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    1.20 -  ML_file "Interpret/mathengine.sml"    (*!part.*)
    1.21 +  ML_file "Interpret/mathengine.sml"    (*!part. WN130804: +check Interpret/me.sml*)
    1.22    ML {*"%%%%%%%%%%%%%%%%% end Interpret.thy %%%%%%%%%%%%%%%%%%%%";*}
    1.23    ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.24    ML_file "xmlsrc/mathml.sml"           (*part.*)
    1.25 @@ -118,8 +118,8 @@
    1.26    ML_file "Knowledge/rootrat.sml"
    1.27    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
    1.28    ML_file "Knowledge/partial_fractions.sml"
    1.29 -  ML_file "Knowledge/polyeq.sml" (*-----------------works if cut into parts !!!!!!!!!!!*)
    1.30 -(*ML_file "Knowledge/rlang.sml"     much to clean up, not urgent due to similar tests  *)
    1.31 +  ML_file "Knowledge/polyeq.sml"
    1.32 +(*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
    1.33    ML_file "Knowledge/calculus.sml"
    1.34    ML_file "Knowledge/trig.sml"
    1.35  (*ML_file "Knowledge/logexp.sml"    not included as stuff for presentation of authoring*) 
    1.36 @@ -138,8 +138,6 @@
    1.37    ML_file "Knowledge/build_thydata.sml"
    1.38    ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.39    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.40 -  ML {*"%%%%%%%%%%%%%%%%% all tests successful %%%%%%%%%%%%%%%%%";*}
    1.41 -  ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.42  
    1.43  section {* history of tests *}
    1.44  text {*