theory Test
imports "../NewParser"
begin

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


declare [[STEPS = 2]]

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 trm =
  Vr "name"
| Ap "trm" "trm list"
| Lm x::"name" t::"trm"  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