1 theory Test

     2 imports "../NewParser"

     3 begin

     4 

     5 declare [[STEPS = 4]]

     6 

     7 atom_decl name

     8 

     9 (*

    10 nominal_datatype trm =

    11   Vr "name"

    12 | Ap "trm" "trm"

    13 

    14 thm fv_trm_raw.simps[no_vars]

    15 *)

    16 

    17 (* This file contains only the examples that are not supposed to work yet. *)

    18 

    19 

    20 declare [[STEPS = 2]]

    21 

    22 

    23 (* example 4 from Terms.thy *)

    24 (* fv_eqvt does not work, we need to repaire defined permute functions

    25    defined fv and defined alpha... *)

    26 (* lists-datastructure does not work yet *)

    27 

    28 nominal_datatype trm =

    29   Vr "name"

    30 | Ap "trm" "trm list"

    31 | Lm x::"name" t::"trm"  bind x in t

    32 

    33 (*

    34 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]

    35 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]

    36 *)

    37 

    38 end

    39 

    40