theory Test
imports "../Parser"
begin

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


atom_decl name

(* example 4 from Terms.thy *)
(* fv_eqvt does not work, we need to repaire defined permute functions
   defined fv and defined alpha... *)
(* lists-datastructure does not work yet
nominal_datatype trm4 =
  Vr4 "name"
| Ap4 "trm4" "trm4 list"
| Lm4 x::"name" t::"trm4"  bind x in t

thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]
thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
*)

end