1.1 --- a/doc-src/isac/jrocnik/Test_Z_Transform.thy	Fri Jul 22 14:01:52 2011 +0200
     1.2 +++ b/doc-src/isac/jrocnik/Test_Z_Transform.thy	Fri Jul 22 15:55:15 2011 +0200
     1.3 @@ -72,6 +72,9 @@
     1.4  
     1.5  *}
     1.6  ML {*
     1.7 +@{term "LENGTH"};
     1.8 +val t = str2term "LENGTH [x+y=1,y=2] = 2";
     1.9 +
    1.10  *}
    1.11  ML {*
    1.12  *}

     2.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml	Fri Jul 22 14:01:52 2011 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml	Fri Jul 22 15:55:15 2011 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4  "----------- the rules -------------------------------------------";
     2.5  "----------- the rules -------------------------------------------";
     2.6  "----------- the rules -------------------------------------------";
     2.7 -fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
     2.8 +fun str2term str = (term_of o the o (parse thy)) str;
     2.9  fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t;
    2.10  fun rewrit thm str = 
    2.11      fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));

     3.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Fri Jul 22 14:01:52 2011 +0200
     3.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Fri Jul 22 15:55:15 2011 +0200
     3.3 @@ -49,32 +49,32 @@
     3.4  
     3.5  (*=== inhibit exn 110722=============================================================
     3.6  
     3.7 -val t = str2term"[c,c_2] from_ [c,c_2,c_3] occur_exactly_in \
     3.8 +val t = str2term"[c,c_2] from [c,c_2,c_3] occur_exactly_in \
     3.9  		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
    3.10  val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
    3.11 -if str = "[c, c_2] from_ [c, c_2,\n                c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True" then ()
    3.12 +if str = "[c, c_2] from [c, c_2,\n                c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = True" then ()
    3.13  else error "eval_occur_exactly_in [c, c_2]";
    3.14  
    3.15 -val t = str2term"[c,c_2,c_3] from_ [c,c_2,c_3] occur_exactly_in \
    3.16 +val t = str2term"[c,c_2,c_3] from [c,c_2,c_3] occur_exactly_in \
    3.17  		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
    3.18  val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
    3.19  if str = "[c, c_2,\n c_3] from_ [c, c_2,\n             c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
    3.20  else error "eval_occur_exactly_in [c, c_2, c_3]";
    3.21  
    3.22 -val t = str2term"[c_2] from_ [c,c_2,c_3] occur_exactly_in \
    3.23 +val t = str2term"[c_2] from [c,c_2,c_3] occur_exactly_in \
    3.24  		\-1 * q_0 * L ^^^ 2 / 2 + L * c + c_2";
    3.25  val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
    3.26  if str = "[c_2] from_ [c, c_2,\n             c_3] occur_exactly_in -1 * q_0 * L ^^^ 2 / 2 + L * c + c_2 = False" then ()
    3.27  else error "eval_occur_exactly_in [c, c_2, c_3]";
    3.28  
    3.29 -val t = str2term"[] from_ [c,c_2,c_3] occur_exactly_in 0";
    3.30 +val t = str2term"[] from [c,c_2,c_3] occur_exactly_in 0";
    3.31  val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
    3.32  if str = "[] from_ [c, c_2, c_3] occur_exactly_in 0 = True" then ()
    3.33  else error "eval_occur_exactly_in [c, c_2, c_3]";
    3.34  
    3.35  val t = 
    3.36      str2term
    3.37 -	"[] from_ [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
    3.38 +	"[] from [c, c_2, c_3, c_4] occur_exactly_in -1 * (q_0 * L ^^^ 2) /2";
    3.39  val SOME (str, t') = eval_occur_exactly_in 0 "EqSystem.occur'_exactly'_in" t 0;
    3.40  if str = "[] from_ [c, c_2, c_3, c_4] occur_exactly_in \
    3.41  	 \-1 * (q_0 * L ^^^ 2) / 2 = True" then ()
    3.42 @@ -84,7 +84,7 @@
    3.43  "----------- problems --------------------------------------------";
    3.44  "----------- problems --------------------------------------------";
    3.45  "----------- problems --------------------------------------------";
    3.46 -val t = str2term "length_ [x+y=1,y=2] = 2";
    3.47 +val t = str2term "LENGTH [x+y=1,y=2] = 2";
    3.48  atomty t;
    3.49  val testrls = append_rls "testrls" e_rls 
    3.50  			 [(Thm ("length_Nil_",num_str @{thm length_Nil_})),