src/HOL/Induct/SList.thy
changeset 61943 7fba644ed827
parent 60530 44f9873d6f6f
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/Induct/SList.thy	Sun Dec 27 21:46:36 2015 +0100
     1.2 +++ b/src/HOL/Induct/SList.thy	Sun Dec 27 22:07:17 2015 +0100
     1.3 @@ -10,8 +10,8 @@
     1.4  
     1.5  Definition of type 'a list (strict lists) by a least fixed point
     1.6  
     1.7 -We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
     1.8 -and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
     1.9 +We use          list(A) == lfp(%Z. {NUMB(0)} <+> A \<times> Z)
    1.10 +and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) \<times> Z)
    1.11  
    1.12  so that list can serve as a "functor" for defining other recursive types.
    1.13