src/HOL/ex/SList.thy
changeset 2911 8a680e310f04
parent 1908 55d8e38262a8
     1.1 --- a/src/HOL/ex/SList.thy	Fri Apr 04 16:16:35 1997 +0200
     1.2 +++ b/src/HOL/ex/SList.thy	Fri Apr 04 16:27:39 1997 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4  
     1.5    list_rec_def
     1.6     "list_rec l c d == 
     1.7 -   List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
     1.8 +   List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
     1.9  
    1.10    (* Generalized Map Functionals *)
    1.11