86 val t = str2term "length_ [x+y=1,y=2] = 2"; |
86 val t = str2term "length_ [x+y=1,y=2] = 2"; |
87 atomty t; |
87 atomty t; |
88 val testrls = append_rls "testrls" e_rls |
88 val testrls = append_rls "testrls" e_rls |
89 [(Thm ("length_Nil_",num_str @{thm length_Nil_})), |
89 [(Thm ("length_Nil_",num_str @{thm length_Nil_})), |
90 (Thm ("length_Cons_",num_str @{thm length_Cons_})), |
90 (Thm ("length_Cons_",num_str @{thm length_Cons_})), |
91 Calc ("op +", eval_binop "#add_"), |
91 Calc ("Groups.plus_class.plus", eval_binop "#add_"), |
92 Calc ("op =",eval_equal "#equal_") |
92 Calc ("op =",eval_equal "#equal_") |
93 ]; |
93 ]; |
94 val SOME (t',_) = rewrite_set_ thy false testrls t; |
94 val SOME (t',_) = rewrite_set_ thy false testrls t; |
95 if term2str t' = "True" then () |
95 if term2str t' = "True" then () |
96 else raise error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; |
96 else raise error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; |
723 nth_ (2 + - 1 + - 1) [] |
723 nth_ (2 + - 1 + - 1) [] |
724 #### rls: erls_prls_triangular on: 1 < 2 + - 1 |
724 #### rls: erls_prls_triangular on: 1 < 2 + - 1 |
725 ##### try calc: op <' |
725 ##### try calc: op <' |
726 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"] |
726 ### asms accepted: ["1 < 2 + - 1"] stored: ["1 < 2 + -1"] |
727 |
727 |
728 ... i.e Calc ("op +", eval_binop "#add_") was missing in erls_prls_triangular*) |
728 ... i.e Calc ("Groups.plus_class.plus", eval_binop "#add_") was missing in erls_prls_triangular*) |
729 trace_rewrite:=false; |
729 trace_rewrite:=false; |
730 (*WN051014------------------------------------------------------------------*) |
730 (*WN051014------------------------------------------------------------------*) |
731 |
731 |
732 "----- relaxed preconditions for triangular system"; |
732 "----- relaxed preconditions for triangular system"; |
733 val fmz = ["equalities [L * q_0 = c, \ |
733 val fmz = ["equalities [L * q_0 = c, \ |