diff -r 16d56796f5a0 -r d679c1f837a7 src/Tools/isac/Build_Isac.thy --- a/src/Tools/isac/Build_Isac.thy Mon Sep 13 17:21:22 2010 +0200 +++ b/src/Tools/isac/Build_Isac.thy Mon Sep 13 18:12:15 2010 +0200 @@ -57,18 +57,11 @@ ML {* writeln "**** build math-engine complete **************************" *} ML {* writeln "**** build the Knowledge *********************************" *} -(**) -use_thy "Knowledge/Delete" +(*use_thy "Knowledge/Delete" use_thy "Knowledge/Descript" use_thy "Knowledge/Atools" use_thy "Knowledge/Simplify" use_thy "Knowledge/Poly" - -ML {* -val m = (1,[2]); -#1 m; -fst m; -*} use_thy "Knowledge/Rational" use_thy "Knowledge/PolyMinus" use_thy "Knowledge/Equation" @@ -89,16 +82,9 @@ use_thy "Knowledge/EqSystem" use_thy "Knowledge/Biegelinie" use_thy "Knowledge/AlgEin" - use_thy "Knowledge/Test" - -ML {* 111; -*} - + use_thy "Knowledge/Test" +*) use_thy "Knowledge/Isac" - -text {*------------------------------------------*} -(* -*) end