src/HOL/BNF/Examples/Misc_Data.thy
changeset 49601 ba31032887db
parent 49510 ba50d204095e
child 51744 0468af6546ff
equal deleted inserted replaced
49599:e716209814b3 49601:ba31032887db
    18 
    18 
    19 data 'a mylist = MyNil | MyCons 'a "'a mylist"
    19 data 'a mylist = MyNil | MyCons 'a "'a mylist"
    20 
    20 
    21 data ('b, 'c, 'd, 'e) some_passive =
    21 data ('b, 'c, 'd, 'e) some_passive =
    22   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
    22   SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
       
    23 
       
    24 data hfset = HFset "hfset fset"
    23 
    25 
    24 data lambda =
    26 data lambda =
    25   Var string |
    27   Var string |
    26   App lambda lambda |
    28   App lambda lambda |
    27   Abs string lambda |
    29   Abs string lambda |