143 (thy, ptp, E, (l @ [Celem.R]), e, a, v); |
143 (thy, ptp, E, (l @ [Celem.R]), e, a, v); |
144 appy thy ptp E (l @ [Celem.R]) e a v; |
144 appy thy ptp E (l @ [Celem.R]) e a v; |
145 |
145 |
146 "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) = |
146 "~~~~~ fun appy, args:"; val (((th,sr)), (pt, p), E, l, t, a, v) = |
147 (thy, ptp, E, (l @ [Celem.R]), e, a, v); |
147 (thy, ptp, E, (l @ [Celem.R]), e, a, v); |
148 val (a', STac stac) = (*case*) handle_leaf "next " th sr E a v t (*of*); |
148 val (a', STac stac) = (*case*) handle_leaf "next " th sr (E, (a, v)) t (*of*); |
149 |
149 |
150 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, E, a, v, t) = ("next ", th, sr, E, a, v, t); |
150 "~~~~~ fun handle_leaf , args:"; val (call, thy, srls, (E, (a, v)), t) = ("next ", th, sr, (E, (a, v)), t); |
151 (*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)), |
151 (*+*)val [(Free ("t_t", Tt_t), Const ("HOL.eq", _) $ (Const ("Groups.plus_class.plus", _) $ Free ("-1", _) $ Free ("x", _)) $ Free ("0", _)), |
152 (Free ("v", Tv), Free ("x", Tx))] = E (* THE WRONG TYPES IN E ..(TODO.4)*) |
152 (Free ("v", Tv), Free ("x", Tx))] = E (* THE WRONG TYPES IN E ..(TODO.4)*) |
153 |
153 |
154 (*+*)val TFree ("'z", ["HOL.type"]) = Tt_t; |
154 (*+*)val TFree ("'z", ["HOL.type"]) = Tt_t; |
155 (*+*)val Type ("Real.real",[]) = Tv; |
155 (*+*)val Type ("Real.real",[]) = Tv; |