src/Tools/isac/Build_Isac.thy
branchisac-update-Isa09-2
changeset 38007 d679c1f837a7
parent 38006 16d56796f5a0
child 38008 79b6cbd02681
     1.1 --- a/src/Tools/isac/Build_Isac.thy	Mon Sep 13 17:21:22 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Sep 13 18:12:15 2010 +0200
     1.3 @@ -57,18 +57,11 @@
     1.4  ML {* writeln "**** build math-engine complete **************************" *}
     1.5  
     1.6  ML {* writeln "**** build the Knowledge *********************************" *}
     1.7 -(**)
     1.8 -use_thy "Knowledge/Delete"
     1.9 +(*use_thy "Knowledge/Delete"
    1.10    use_thy "Knowledge/Descript"
    1.11    use_thy "Knowledge/Atools"
    1.12    use_thy "Knowledge/Simplify"
    1.13    use_thy "Knowledge/Poly"
    1.14 -
    1.15 -ML {*
    1.16 -val m = (1,[2]);
    1.17 -#1 m;
    1.18 -fst m;
    1.19 -*}
    1.20    use_thy "Knowledge/Rational"
    1.21    use_thy "Knowledge/PolyMinus"
    1.22    use_thy "Knowledge/Equation"
    1.23 @@ -89,16 +82,9 @@
    1.24    use_thy "Knowledge/EqSystem"
    1.25    use_thy "Knowledge/Biegelinie"
    1.26    use_thy "Knowledge/AlgEin"
    1.27 - use_thy "Knowledge/Test"
    1.28 -
    1.29 -ML {* 111;
    1.30 -*}
    1.31 -
    1.32 +  use_thy "Knowledge/Test"
    1.33 +*)
    1.34  use_thy "Knowledge/Isac"
    1.35  
    1.36 -
    1.37 -text {*------------------------------------------*}
    1.38 -(*
    1.39 -*)
    1.40  end
    1.41