1.1 --- a/test/Tools/isac/Knowledge/diff.sml	Tue Aug 31 16:00:13 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diff.sml	Tue Aug 31 16:38:22 2010 +0200
     1.3 @@ -53,17 +53,17 @@
     1.4       [("erls",
     1.5         Rls {id = "erls",preconds = [], rew_ord = ("termlessI",termlessI), 
     1.6  	    erls = e_rls, srls = Erls, calc = [], (*asm_thm = [],*)
     1.7 -	    rules = [Thm ("refl",num_str refl),
     1.8 -		     Thm ("le_refl",num_str le_refl),
     1.9 -		     Thm ("radd_left_cancel_le",num_str radd_left_cancel_le),
    1.10 -		     Thm ("not_true",num_str not_true),
    1.11 -		     Thm ("not_false",num_str not_false),
    1.12 +	    rules = [Thm ("refl",num_str @{refl),
    1.13 +		     Thm ("real_le_refl",num_str @{thm real_le_refl}),
    1.14 +		     Thm ("radd_left_cancel_le",num_str @{radd_left_cancel_le),
    1.15 +		     Thm ("not_true",num_str @{not_true),
    1.16 +		     Thm ("not_false",num_str @{not_false),
    1.17  		     Thm ("and_true",and_true),
    1.18  		     Thm ("and_false",and_false),
    1.19  		     Thm ("or_true",or_true),
    1.20  		     Thm ("or_false",or_false),
    1.21 -		     Thm ("and_commute",num_str and_commute),
    1.22 -		     Thm ("or_commute",num_str or_commute),
    1.23 +		     Thm ("and_commute",num_str @{and_commute),
    1.24 +		     Thm ("or_commute",num_str @{or_commute),
    1.25  		     
    1.26  		     Calc ("Atools.is'_const",eval_const "#is_const_"),
    1.27  		     Calc ("Atools.occurs'_in", eval_occurs_in ""),
    1.28 @@ -270,7 +270,7 @@
    1.29   val SOME (t'',_) = rewrite_set_ Isac.thy false make_polynomial t';
    1.30   term2str t'';
    1.31   
    1.32 - val thm = num_str realpow_eq_oneI;
    1.33 + val thm = num_str @{realpow_eq_oneI;
    1.34   case string_of_thm thm of
    1.35  
    1.36