theory Testimports "../NewParser"begindeclare [[STEPS = 4]]atom_decl name(*nominal_datatype trm = Vr "name"| Ap "trm" "trm"thm fv_trm_raw.simps[no_vars]*)(* This file contains only the examples that are not supposed to work yet. *)declare [[STEPS = 2]](* 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