closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
theory Testimports "../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 yetnominal_datatype trm4 = Vr4 "name"| Ap4 "trm4" "trm4 list"| Lm4 x::"name" t::"trm4" bind x in tthm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars]thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*)(* example 8 from Terms.thy *)(* Binding in a term under a bn, needs to fail *)(*nominal_datatype foo8 = Foo0 "name"| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"and bar8 = Bar0 "name"| Bar1 "name" s::"name" b::"bar8" bind s in bbinder bv8where "bv8 (Bar0 x) = {}"| "bv8 (Bar1 v x b) = {atom v}"*)end