2 imports "../NewParser"

     2 imports "../NewParser"

     3 begin

     3 begin

     4 

     4 

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

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

     6 

     6 

     7 

     9 

     8 atom_decl name

    10 atom_decl name

     9 

    11 

    10 (* example 4 from Terms.thy *)

    12 (* example 4 from Terms.thy *)

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

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

    12    defined fv and defined alpha... *)

    14    defined fv and defined alpha... *)

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

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

    14 

    16 

    16 nominal_datatype trm =

    17 nominal_datatype trm =

    17   Vr "name"

    18   Vr "name"

    18 | Ap "trm" "trm list"

    19 | Ap "trm" "trm list"

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

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

    21 

    22 

    22 (*

    23 (*

    23 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]

    24 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]

    24 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]

    25 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]

    25 *)

    26 *)