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