test/Tools/isac/Knowledge/complex.sml
branchisac-update-Isa09-2
changeset 37967 bd4f7a35e892
parent 37960 ec20007095f2
     1.1 --- a/test/Tools/isac/Knowledge/complex.sml	Tue Aug 31 16:00:13 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/complex.sml	Tue Aug 31 16:38:22 2010 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4   val SOME (t',_) = 
     1.5       rewrite_set_ thy false 
     1.6  		  (append_rls "simpl_complex" make_polynomial 
     1.7 -			      [Thm ("square_I", num_str square_I)]) t;
     1.8 +			      [Thm ("square_I", num_str @{square_I)]) t;
     1.9   term2str t';
    1.10   "Float ((363, -2), 0, 0) + I__ * Float ((484, -2), 0, 0) +\
    1.11   \I__ * Float ((726, -2), 0, 0) + -1 * Float ((968, -2), 0, 0)"