branch | isac-update-Isa09-2 |
changeset 37969 | 81922154e742 |
parent 37967 | bd4f7a35e892 |
child 37979 | 4f11d7840684 |
1.1 --- a/test/Tools/isac/Knowledge/rational.sml Wed Sep 01 09:56:09 2010 +0200 1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Sep 01 15:17:43 2010 +0200 1.3 @@ -983,7 +983,7 @@ 1.4 "True"; 1.5 val t = str2term "(6*x)^^^2"; 1.6 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false 1.7 - (num_str @{realpow_def_atom) t; 1.8 + (num_str @{thm realpow_def_atom) t; 1.9 term2str t'; 1.10 trace_rewrite:=false; 1.11