equal
deleted
inserted
replaced
92 ]; |
92 ]; |
93 val SOME (t',_) = rewrite_set_ thy false testrls t; |
93 val SOME (t',_) = rewrite_set_ thy false testrls t; |
94 if UnparseC.term t' = "True" then () |
94 if UnparseC.term t' = "True" then () |
95 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; |
95 else error "eqsystem.sml: length_ [x+y=1,y=2] = 2"; |
96 |
96 |
97 val SOME t = TermC.parse thy "solution LL"; |
97 val SOME t = TermC.parseNEW ctxt "solution LL"; |
98 TermC.atomty (Thm.term_of t); |
98 TermC.atomty t; |
99 val SOME t = TermC.parse thy "solution LL"; |
99 val SOME t = TermC.parseNEW ctxt "solution LL"; |
100 TermC.atomty (Thm.term_of t); |
100 TermC.atomty t; |
101 |
101 |
102 val t = TermC.str2term |
102 val t = TermC.str2term |
103 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"; |
103 "(tl (tl (tl v_s))) from v_s occur_exactly_in (NTH 1 (e_s::bool list))"; |
104 TermC.atomty t; |
104 TermC.atomty t; |
105 val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^ |
105 val t = TermC.str2term ("(tl (tl (tl [c, c_2, c_3, c_4]))) from [c, c_2, c_3, c_4] occur_exactly_in " ^ |