src/Doc/Tutorial/ToyList/ToyList1.txt
changeset 58372 bfd497f2f4c2
parent 58112 8081087096ad
child 58926 baf5a3c28f0c
equal deleted inserted replaced
58371:7f30ec82fe40 58372:bfd497f2f4c2
     1 theory ToyList
     1 theory ToyList
     2 imports Old_Datatype
     2 imports BNF_Least_Fixpoint
     3 begin
     3 begin
     4 
     4 
     5 datatype 'a list = Nil                          ("[]")
     5 datatype 'a list = Nil                          ("[]")
     6                  | Cons 'a "'a list"            (infixr "#" 65)
     6                  | Cons 'a "'a list"            (infixr "#" 65)
     7 
     7