| changeset 725 | d9c629fbacc6 |
| parent 0 | a5a9c433f639 |
| child 755 | dfb3894d78e4 |
--- a/src/FOL/ex/List.ML Mon Nov 21 14:06:59 1994 +0100 +++ b/src/FOL/ex/List.ML Mon Nov 21 14:11:21 1994 +0100 @@ -11,7 +11,7 @@ val prems = goal List.thy "[| P([]); !!x l. P(x.l) |] ==> All(P)"; by (rtac list_ind 1); by (REPEAT (resolve_tac (prems@[allI,impI]) 1)); -val list_exh = result(); +qed "list_exh"; val list_rew_thms = [list_distinct1,list_distinct2,app_nil,app_cons, hd_eq,tl_eq,forall_nil,forall_cons,list_free,