test/Tools/isac/Test_Isac.thy
changeset 42407 81afb8eb9b03
parent 42400 dcacb8077a98
child 42412 52cb88544681
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Apr 05 17:08:48 2012 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Tue Apr 10 09:31:21 2012 +0200
     1.3 @@ -95,6 +95,7 @@
     1.4    ("Knowledge/algein.sml")
     1.5    ("Knowledge/diophanteq.sml")
     1.6    ("Knowledge/isac.sml")
     1.7 +  ("Knowledge/build_thydata.sml")
     1.8  
     1.9  begin
    1.10  
    1.11 @@ -127,7 +128,7 @@
    1.12    use "Interpret/generate.sml"
    1.13    use "Interpret/calchead.sml"      (*part.*)
    1.14    use "Interpret/appl.sml"          (*!complete WEGEN INTERMED TESTCODE*)
    1.15 -  use "Interpret/rewtools.sml"      (*TODO*)
    1.16 +  use "Interpret/rewtools.sml"      (*TODO/part.WN120406*)
    1.17    use "Interpret/script.sml"        (*!TODO/part.*)
    1.18    use "Interpret/solve.sml"         (*part.*)
    1.19    use "Interpret/inform.sml"        (*part.*)
    1.20 @@ -136,15 +137,15 @@
    1.21    ML {*"%%%%%%%%%%%%%%%%% start xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.22    use "xmlsrc/mathml.sml"            (*part.*)
    1.23    use "xmlsrc/datatypes.sml"         (*TODO/part.*)
    1.24 -  use "xmlsrc/pbl-met-hierarchy.sml" (*TODO/part.*)
    1.25 -  use "xmlsrc/thy-hierarchy.sml"     (*TODO after 2009-2/part.*) 
    1.26 +  use "xmlsrc/pbl-met-hierarchy.sml" (*TODO after 2009-2/part.*)
    1.27 +  use "xmlsrc/thy-hierarchy.sml"     (*TODO after 2009-2/part.*)
    1.28    use "xmlsrc/interface-xml.sml"     (*TODO after 2009-2*)
    1.29    ML {*"%%%%%%%%%%%%%%%%% end xmlsrc.thy %%%%%%%%%%%%%%%%%%%%%%%";*}
    1.30    ML {*"%%%%%%%%%%%%%%%%% start Frontend.thy %%%%%%%%%%%%%%%%%%%";*}
    1.31    use "Frontend/messages.sml"
    1.32    use "Frontend/states.sml"
    1.33    use "Frontend/interface.sml"
    1.34 -  use         "print_exn_G.sml"
    1.35 +  use          "print_exn_G.sml"
    1.36    ML {*"%%%%%%%%%%%%%%%%% end Frontend.thy %%%%%%%%%%%%%%%%%%%%%";*}
    1.37    ML {*"%%%%%%%%%%%%%%%%% start Knowledge.thy %%%%%%%%%%%%%%%%%%";*}
    1.38    use "Knowledge/delete.sml"