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