src/Tools/isac/Interpret/appl.sml
branchisac-update-Isa09-2
changeset 38050 4c52ad406c20
parent 38031 460c24a6a6ba
child 38053 bb6004e10e71
     1.1 --- a/src/Tools/isac/Interpret/appl.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/appl.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -165,12 +165,12 @@
     1.4  (*before 5.03-----
     1.5  > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #3) + sqrt (#5 - #3)) &\
     1.6  	   \ #0 <= #25 + #-1 * #3 ^^^ #2) & #0 <= #4";
     1.7 -> val SOME(ct',_) = rewrite_set "Isac.thy" false "eval_rls" ct;
     1.8 +> val SOME(ct',_) = rewrite_set "Isac" false "eval_rls" ct;
     1.9  val ct' = "True" : cterm'
    1.10  
    1.11  > val ct = "((#0 <= #18 & #0 <= sqrt (#5 + #-3) + sqrt (#5 - #-3)) &\
    1.12  	   \ #0 <= #25 + #-1 * #-3 ^^^ #2) & #0 <= #4";
    1.13 -> val SOME(ct',_) = rewrite_set "Isac.thy"  false "eval_rls" ct;
    1.14 +> val SOME(ct',_) = rewrite_set "Isac"  false "eval_rls" ct;
    1.15  val ct' = "True" : cterm'
    1.16  
    1.17