| changeset 1294 | 1358dc040edb |
| parent 0 | a5a9c433f639 |
| child 1459 | d12da312eff4 |
--- a/src/CTT/ex/equal.ML Tue Oct 24 14:42:15 1995 +0100 +++ b/src/CTT/ex/equal.ML Tue Oct 24 14:45:35 1995 +0100 @@ -11,7 +11,7 @@ by (rtac EqE 1); by (resolve_tac elim_rls 1 THEN resolve_tac prems 1); by (rew_tac prems); -val split_eq = result(); +qed "split_eq"; val prems = goal CTT.thy @@ -19,7 +19,7 @@ by (rtac EqE 1); by (resolve_tac elim_rls 1 THEN resolve_tac prems 1); by (rew_tac prems); -val when_eq = result(); +qed "when_eq"; (*in the "rec" formulation of addition, 0+n=n *)