theory Test+ −
imports "../NewParser"+ −
begin+ −
+ −
declare [[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+ −
+ −
+ −