test/Tools/isac/Knowledge/diffapp.sml
branchdecompose-isar
changeset 41928 20138d6136cd
parent 38043 6a36acec95d9
child 41943 f33f6959948b
     1.1 --- a/test/Tools/isac/Knowledge/diffapp.sml	Thu Mar 10 15:19:26 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml	Thu Mar 10 16:04:00 2011 +0100
     1.3 @@ -488,7 +488,7 @@
     1.4  "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]";
     1.5  val SOME (s',_) = rewrite_set_ thy false list_rls s;
     1.6  val s'' = term2str s';
     1.7 -if s''="True" then () else error "new behaviour with list_rls 1.2.";
     1.8 +if s''="HOL.True" then () else error "new behaviour with list_rls 1.2.";
     1.9  
    1.10  (*--- 2.line in script ---*)
    1.11  val t = str2term