269 val ets0=[([],(Tac_(Program.thy,"BS", "", ""),[(eq_,ve0_)],[(eq_,ve0_)], |
269 val ets0=[([],(Tac_(Program.thy,"BS", "", ""),[(eq_,ve0_)],[(eq_,ve0_)], |
270 TermC.empty,TermC.empty,Safe)), |
270 TermC.empty,TermC.empty,Safe)), |
271 ([],(User', [], [], TermC.empty, TermC.empty,Sundef))]:ets; |
271 ([],(User', [], [], TermC.empty, TermC.empty,Sundef))]:ets; |
272 val l0 = []; |
272 val l0 = []; |
273 " --------------- 1. ---------------------------------------------"; |
273 " --------------- 1. ---------------------------------------------"; |
274 val (pt,_) = cappend_atomic pt[1]Istate.empty TermC.empty(Rewrite("test", ""))(TermC.parse_test @{context} ct,[])Complete; |
274 val (pt,_) = cappend_atomic pt[1]Istate.empty TermC.empty(Rewrite("test", ""))(ParseC.parse_test @{context} ct,[])Complete; |
275 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv" |
275 (*12.10.03:*** Unknown theorem(s) "rroot_square_inv" |
276 val Applicable.Yes m' = Step.check (Rewrite("rroot_square_inv", "")) (pt, p); |
276 val Applicable.Yes m' = Step.check (Rewrite("rroot_square_inv", "")) (pt, p); |
277 *) |
277 *) |
278 |
278 |
279 |
279 |