List.ML

--- a/List.ML	Thu Aug 18 12:38:12 1994 +0200
+++ b/List.ML	Thu Aug 18 12:42:19 1994 +0200
@@ -1,9 +1,9 @@
-(*  Title: 	HOL/list
+(*  Title: 	HOL/List
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For list.thy.  
+For List.thy.  
 *)
 
 open List;
@@ -172,11 +172,11 @@
 
 (** Conversion rules for List_case: case analysis operator **)
 
-goalw List.thy [List_case_def,NIL_def] "List_case(NIL,c,h) = c";
+goalw List.thy [List_case_def,NIL_def] "List_case(c, h, NIL) = c";
 by (rtac Case_In0 1);
 val List_case_NIL = result();
 
-goalw List.thy [List_case_def,CONS_def]  "List_case(CONS(M,N), c, h) = h(M,N)";
+goalw List.thy [List_case_def,CONS_def]  "List_case(c, h, CONS(M,N)) = h(M,N)";
 by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1);
 val List_case_CONS = result();
 
@@ -213,20 +213,20 @@
 
 goal List.thy "List_rec(NIL,c,h) = c";
 by (rtac (List_rec_unfold RS trans) 1);
-by (rtac List_case_NIL 1);
+by (simp_tac (HOL_ss addsimps [List_case_NIL]) 1);
 val List_rec_NIL = result();
 
 goal List.thy "!!M. [| M: Sexp;  N: Sexp |] ==> \
 \    List_rec(CONS(M,N), c, h) = h(M, N, List_rec(N,c,h))";
 by (rtac (List_rec_unfold RS trans) 1);
-by (rtac (List_case_CONS RS trans) 1);
-by(asm_simp_tac(HOL_ss addsimps [CONS_I, pred_Sexp_CONS_I2, cut_apply])1);
+by (asm_simp_tac
+    (HOL_ss addsimps [List_case_CONS, CONS_I, pred_Sexp_CONS_I2, cut_apply])1);
 val List_rec_CONS = result();
 
 (*** list_rec -- by List_rec ***)
 
 val Rep_List_in_Sexp =
-    Rep_List RS (range_Leaf_subset_Sexp RS List_subset_Sexp RS subsetD);
+    [range_Leaf_subset_Sexp RS List_subset_Sexp, Rep_List] MRS subsetD;
 
 local
   val list_rec_simps = list_free_simps @
@@ -392,7 +392,7 @@
 (** list_case **)
 
 goal List.thy
- "P(list_case(xs,a,f)) = ((xs=[] --> P(a)) & \
+ "P(list_case(a,f,xs)) = ((xs=[] --> P(a)) & \
 \                         (!y ys. xs=y#ys --> P(f(y,ys))))";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac list_ss));