1 theory Term8

     2 imports "../NewParser"

     3 begin

     4 

     5 (* example 8 *)

     6 

     7 atom_decl name

     8 

     9 nominal_datatype foo =

    10   Foo0 "name"

    11 | Foo1 b::"bar" f::"foo" bind (set) "bv b" in f

    12 and bar =

    13   Bar0 "name"

    14 | Bar1 "name" s::"name" b::"bar" bind (set) s in b

    15 binder

    16   bv

    17 where

    18   "bv (Bar0 x) = {}"

    19 | "bv (Bar1 v x b) = {atom v}"

    20 

    21 (*

    22 thm foo_bar.supp

    23 *)

    24 

    25 end

    26 

    27