# HG changeset patch # User Cezary Kaliszyk # Date 1272889871 -7200 # Node ID 7f504136149b6f6aac0d0905b2bd68f299a451a0 # Parent 070ba8972e97ca2b93b58d5a43dc59a8c08a73c0 Another example where only alpha_eqvt fails. diff -r 070ba8972e97 -r 7f504136149b Nominal/Ex/Ex2.thy --- a/Nominal/Ex/Ex2.thy Mon May 03 14:30:37 2010 +0200 +++ b/Nominal/Ex/Ex2.thy Mon May 03 14:31:11 2010 +0200 @@ -1,35 +1,33 @@ theory Ex2 -imports "../Parser" +imports "../NewParser" begin text {* example 2 *} atom_decl name -ML {* val _ = recursive := false *} -nominal_datatype trm' = +ML {* val _ = cheat_alpha_eqvt := true *} + +nominal_datatype trm = Var "name" -| App "trm'" "trm'" -| Lam x::"name" t::"trm'" bind x in t -| Let p::"pat'" "trm'" t::"trm'" bind "f p" in t -and pat' = +| App "trm" "trm" +| Lam x::"name" t::"trm" bind_set x in t +| Let p::"pat" "trm" t::"trm" bind_set "f p" in t +and pat = PN | PS "name" | PD "name" "name" binder - f::"pat' \ atom set" + f::"pat \ atom set" where "f PN = {}" | "f (PD x y) = {atom x, atom y}" | "f (PS x) = {atom x}" - -thm trm'_pat'.fv -thm trm'_pat'.eq_iff -thm trm'_pat'.bn -thm trm'_pat'.perm -thm trm'_pat'.induct -thm trm'_pat'.distinct -thm trm'_pat'.fv[simplified trm'_pat'.supp] +thm trm_pat.bn +thm trm_pat.perm +thm trm_pat.induct +thm trm_pat.distinct +thm trm_pat.fv[simplified trm_pat.supp(1-2)] end