equal
deleted
inserted
replaced
486 val s = subst_atomic env t; |
486 val s = subst_atomic env t; |
487 term2str s; |
487 term2str s; |
488 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"; |
488 "1 < length_ [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"; |
489 val SOME (s',_) = rewrite_set_ thy false list_rls s; |
489 val SOME (s',_) = rewrite_set_ thy false list_rls s; |
490 val s'' = term2str s'; |
490 val s'' = term2str s'; |
491 if s''="True" then () else error "new behaviour with list_rls 1.2."; |
491 if s''="HOL.True" then () else error "new behaviour with list_rls 1.2."; |
492 |
492 |
493 (*--- 2.line in script ---*) |
493 (*--- 2.line in script ---*) |
494 val t = str2term |
494 val t = str2term |
495 "(if 1 < length_ r_s \ |
495 "(if 1 < length_ r_s \ |
496 \ then (SubProblem (Reals_,[make,function],[no_met])\ |
496 \ then (SubProblem (Reals_,[make,function],[no_met])\ |