src/HOL/ex/LList.thy
changeset 2911 8a680e310f04
parent 1824 44254696843a
child 2986 dbd42504b9fa
     1.1 --- a/src/HOL/ex/LList.thy	Fri Apr 04 16:16:35 1997 +0200
     1.2 +++ b/src/HOL/ex/LList.thy	Fri Apr 04 16:27:39 1997 +0200
     1.3 @@ -89,7 +89,7 @@
     1.4  
     1.5    llist_case_def
     1.6     "llist_case c d l == 
     1.7 -       List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
     1.8 +       List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
     1.9  
    1.10    LList_corec_fun_def
    1.11      "LList_corec_fun k f ==