test/Tools/isac/Knowledge/rational.sml
branchdecompose-isar
changeset 41928 20138d6136cd
parent 38083 a1d13f3de312
child 41929 e4b645e5f25b
     1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Thu Mar 10 15:19:26 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Thu Mar 10 16:04:00 2011 +0100
     1.3 @@ -1005,10 +1005,10 @@
     1.4  (*trace_rewrite:=true;*)
     1.5  val t = str2term "Not (6*x is_atom)";
     1.6  val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
     1.7 -"True";
     1.8 +"HOL.True";
     1.9  val t = str2term "1 < 2";
    1.10  val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
    1.11 -"True";
    1.12 +"HOL.True";
    1.13  
    1.14  val t = str2term "(6*x)^^^2";
    1.15  val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false