1.1 --- a/src/Tools/isac/Test_Isac.thy	Tue Oct 05 09:17:48 2010 +0200
     1.2 +++ b/src/Tools/isac/Test_Isac.thy	Tue Oct 05 14:41:16 2010 +0200
     1.3 @@ -80,24 +80,26 @@
     1.4  val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
     1.5  Envir.subst_term subst (*pres?*);
     1.6  *}
     1.7 -ML {*print_depth 5*}
     1.8  use"../../../test/Tools/isac/Knowledge/poly.sml"; (*part.*)
     1.9 -
    1.10 -ML {*theory "Isac";
    1.11 -theory "Poly";
    1.12 -theory "Rational";
    1.13 -theory "Equation";
    1.14 +ML {*
    1.15 +the o (parse thy);
    1.16 +((parse thy)) "9 = 3 ^^^ 2";
    1.17 +(the o (parse thy)) "9 = 3 ^^^ 2";
    1.18 +(term_of o the o (parse thy)) "9 = 3 ^^^ 2";
    1.19 +Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2";
    1.20 +cterm_of (theory "Isac") (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2");
    1.21 +(make_thm o (cterm_of (theory "Isac")))
    1.22 +  (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2");
    1.23  *}
    1.24  
    1.25 -ML {*theory "Isac";
    1.26 -assoc_thy;
    1.27 -cancel;
    1.28 -assoc_thy "Poly";
    1.29 -assoc_thy "Rational";
    1.30 -assoc_thy "Equation";
    1.31 +ML {*
    1.32 +str2term "1 < (2 :: real)";
    1.33  *}
    1.34  
    1.35  use"../../../test/Tools/isac/Knowledge/rational.sml"
    1.36 +
    1.37 +ML {*111*}
    1.38 +
    1.39  (*
    1.40  	use"equation.sml";
    1.41   	use"root.sml";