test/Tools/isac/Test_Isac.thy
branchdecompose-isar
changeset 42321 e68b4b4f0fac
parent 42319 ffad491ba8f2
child 42360 2c8de368c64c
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Oct 14 14:34:10 2011 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Oct 14 16:12:50 2011 +0200
     1.3 @@ -124,7 +124,7 @@
     1.4    use "Interpret/mstools.sml"
     1.5    use "Interpret/ctree.sml"         (*!...!see(25)*)
     1.6    use "Interpret/ptyps.sml"         (*part.*)
     1.7 -(*use "Interpret/generate.sml"        new 2011*)
     1.8 +  use "Interpret/generate.sml"
     1.9    use "Interpret/calchead.sml"      (*part.*)
    1.10    use "Interpret/appl.sml"          (*!complete WEGEN INTERMED TESTCODE*)
    1.11    use "Interpret/rewtools.sml"      (*!    *)
    1.12 @@ -141,14 +141,14 @@
    1.13    use "xmlsrc/interface-xml.sml"     (*TODO after 2009-2*)
    1.14    ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
    1.15    ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
    1.16 -  use "Frontend/messages.sml"        (*new 2011*)
    1.17 -  use "Frontend/states.sml"          (*new 2011*)
    1.18 +  use "Frontend/messages.sml"
    1.19 +  use "Frontend/states.sml"
    1.20    use "Frontend/interface.sml"
    1.21 -  use         "print_exn_G.sml"      (*new 2011*)
    1.22 +  use         "print_exn_G.sml"
    1.23    ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.24    ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
    1.25 -  use "Knowledge/delete.sml"         (*new 2011*)
    1.26 -  use "Knowledge/descript.sml"       (*new 2011*)
    1.27 +  use "Knowledge/delete.sml"
    1.28 +  use "Knowledge/descript.sml"
    1.29  (*use "Knowledge/atools.sml"           2002, added termorder.sml 2011*)
    1.30    use "Knowledge/simplify.sml"       (*part.*)
    1.31  (*use "Knowledge/poly.sml"             2002*)
    1.32 @@ -163,9 +163,9 @@
    1.33    use "Knowledge/partial_fractions.sml"
    1.34    use "Knowledge/polyeq.sml"
    1.35  (*use "Knowledge/rlang.sml"            2002???*)
    1.36 -  use "Knowledge/calculus.sml"       (*new 2011*)
    1.37 +  use "Knowledge/calculus.sml"
    1.38    use "Knowledge/trig.sml"
    1.39 -  use "Knowledge/logexp.sml"         (*part.*) 
    1.40 +(*use "Knowledge/logexp.sml"  not included as stuff for presentation of authoring*) 
    1.41    use "Knowledge/diff.sml"           (*part.*)
    1.42    use "Knowledge/integrate.sml"      (*part. was complete 2009-2
    1.43                                                diff.emacs--jedit*)