test/Tools/isac/Test_Isac.thy
branchdecompose-isar
changeset 42225 7daeeee85596
parent 42218 dbdaf1e4e614
child 42226 7fff709d1a72
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Jul 27 13:05:27 2011 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Jul 28 11:27:04 2011 +0200
     1.3 @@ -100,11 +100,11 @@
     1.4    use          "library.sml"
     1.5    use          "calcelems.sml"
     1.6    use "ProgLang/termC.sml"
     1.7 -  use "ProgLang/calculate.sml"      (*part.*)
     1.8 -  use "ProgLang/rewrite.sml"        (*?complete?*)
     1.9 +  use "ProgLang/calculate.sml"
    1.10 +  use "ProgLang/rewrite.sml"
    1.11  (*use "ProgLang/listC.sml"            2002*)
    1.12 -  use "ProgLang/scrtools.sml"         (*complete*)
    1.13 -  use "ProgLang/tools.sml"            (*complete*)
    1.14 +  use "ProgLang/scrtools.sml"
    1.15 +  use "ProgLang/tools.sml"
    1.16    ML {*"%%%%%%%%%%%%%%%%% end ProgLang.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.17    ML {*"%%%%%%%%%%%%%%%%% start Minisubpbl %%%%%%%%%%%%%%%%%%%%%";*}
    1.18    use "Minisubpbl/000-comments.sml"
    1.19 @@ -141,7 +141,7 @@
    1.20    ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
    1.21    use "Frontend/messages.sml"        (*new 2011*)
    1.22    use "Frontend/states.sml"          (*new 2011*)
    1.23 -  use "Frontend/interface.sml"       (*complete*)                            
    1.24 +  use "Frontend/interface.sml"
    1.25    use         "print_exn_G.sml"      (*new 2011*)
    1.26    ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.27    ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
    1.28 @@ -161,19 +161,19 @@
    1.29  (*use "Knowledge/polyeq.sml"           2002*)
    1.30  (*use "Knowledge/rlang.sml"            2002???*)
    1.31    use "Knowledge/calculus.sml"       (*new 2011*)
    1.32 -  use "Knowledge/trig.sml"           (*complete*)
    1.33 +  use "Knowledge/trig.sml"
    1.34    use "Knowledge/logexp.sml"         (*part.*) 
    1.35    use "Knowledge/diff.sml"           (*part.*)
    1.36    use "Knowledge/integrate.sml"      (*part. was complete 2009-2
    1.37                                                diff.emacs--jedit*)
    1.38    use "Knowledge/eqsystem.sml"       (*part.*)
    1.39 -  use "Knowledge/test.sml"           (*complete*)
    1.40 +  use "Knowledge/test.sml"
    1.41    use "Knowledge/polyminus.sml"      (*part.*)
    1.42 -  use "Knowledge/vect.sml"           (*complete*)
    1.43 +  use "Knowledge/vect.sml"
    1.44    use "Knowledge/diffapp.sml"        (*part.*)
    1.45    use "Knowledge/biegelinie.sml"     (*part.*)
    1.46    use "Knowledge/algein.sml"         (*part.*)
    1.47 -  use "Knowledge/diophanteq.sml"     (*complete*)
    1.48 +  use "Knowledge/diophanteq.sml"
    1.49    use "Knowledge/isac.sml"           (*part.*)
    1.50    ML {*"%%%%%%%%%%%%%%%%% end Knowledge.thy %%%%%%%%%%%%%%%%%%%%";*}
    1.51    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}