test/Tools/isac/Knowledge/eqsystem.sml
branchisac-update-Isa09-2
changeset 38014 3e11e3c2dc42
parent 37995 fac82f29f143
child 38031 460c24a6a6ba
     1.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Thu Sep 23 12:56:51 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Thu Sep 23 14:49:23 2010 +0200
     1.3 @@ -88,7 +88,7 @@
     1.4  val testrls = append_rls "testrls" e_rls 
     1.5  			 [(Thm ("length_Nil_",num_str @{thm length_Nil_})),
     1.6  			  (Thm ("length_Cons_",num_str @{thm length_Cons_})),
     1.7 -			  Calc ("op +", eval_binop "#add_"),
     1.8 +			  Calc ("Groups.plus_class.plus", eval_binop "#add_"),
     1.9  			  Calc ("op =",eval_equal "#equal_")
    1.10  			  ];
    1.11  val SOME (t',_) = rewrite_set_ thy false testrls t;
    1.12 @@ -725,7 +725,7 @@
    1.13  #####  try calc: op <'
    1.14  ###  asms accepted: ["1 < 2 + - 1"]   stored: ["1 < 2 + -1"]
    1.15  
    1.16 -... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*)
    1.17 +... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*)
    1.18  trace_rewrite:=false;
    1.19  (*WN051014------------------------------------------------------------------*)
    1.20