src/HOL/Induct/SList.ML
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 5535 678999604ee9
     1.1 --- a/src/HOL/Induct/SList.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/Induct/SList.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -147,8 +147,7 @@
     1.4  (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
     1.5     hold if pred_sexp^+ were changed to pred_sexp. *)
     1.6  
     1.7 -Goal
     1.8 -   "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
     1.9 +Goal "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
    1.10                             \     (%g. List_case c (%x y. d x y (g y)))";
    1.11  by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
    1.12  val List_rec_unfold = standard 
    1.13 @@ -339,8 +338,7 @@
    1.14  
    1.15  (** list_case **)
    1.16  
    1.17 -Goal
    1.18 - "P(list_case a f xs) = ((xs=[] --> P(a)) & \
    1.19 +Goal "P(list_case a f xs) = ((xs=[] --> P(a)) & \
    1.20  \                        (!y ys. xs=y#ys --> P(f y ys)))";
    1.21  by (list_ind_tac "xs" 1);
    1.22  by (ALLGOALS Asm_simp_tac);