# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272983618 -7200
# Node ID 5a8a3e209b950c11986daa4bbe8e6bf8c5791e5e
# Parent  f2f427bc4fd171e58ed0d3e3a63a6c02d8fd06c8# Parent  58e13de342a5375852b9a38148af15811fdeb94b
merge

diff -r f2f427bc4fd1 -r 5a8a3e209b95 Nominal/Ex/ExPS3.thy
--- a/Nominal/Ex/ExPS3.thy	Tue May 04 16:33:30 2010 +0200
+++ b/Nominal/Ex/ExPS3.thy	Tue May 04 16:33:38 2010 +0200
@@ -1,17 +1,20 @@
 theory ExPS3
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 3 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+ML {* val _ = cheat_alpha_bn_rsp := true *}
+
 nominal_datatype exp =
   VarP "name"
 | AppP "exp" "exp"
-| LamP x::"name" e::"exp" bind x in e
-| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1
+| LamP x::"name" e::"exp" bind_set x in e
+| LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1
 and pat3 =
   PVar "name"
 | PUnit
@@ -30,7 +33,7 @@
 thm exp_pat3.induct
 thm exp_pat3.distinct
 thm exp_pat3.fv
-thm exp_pat3.supp
+thm exp_pat3.supp(1-2)
 
 end
 
diff -r f2f427bc4fd1 -r 5a8a3e209b95 Nominal/Ex/ExPS8.thy
--- a/Nominal/Ex/ExPS8.thy	Tue May 04 16:33:30 2010 +0200
+++ b/Nominal/Ex/ExPS8.thy	Tue May 04 16:33:38 2010 +0200
@@ -1,23 +1,21 @@
 theory ExPS8
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 8 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-(* One function is recursive and the other one is not,
-   and as the parser cannot handle this we cannot set
-   the reference.  *)
-ML {* val _ = recursive := false  *}
+ML {* val _ = cheat_fv_rsp := true *}
+ML {* val _ = cheat_alpha_bn_rsp := true *}
 
 nominal_datatype exp =
   EVar name
 | EUnit
 | EPair exp exp
-| ELetRec l::lrbs e::exp bind "b_lrbs l" in e (* rec *)
+| ELetRec l::lrbs e::exp bind_set "b_lrbs l" in l e
 and fnclause =
-  K x::name p::pat f::exp bind "b_pat p" in f (* non-rec *)
+  K x::name p::pat f::exp bind_set "b_pat p" in f
 and fnclauses =
   S fnclause
 | ORs fnclause fnclauses
@@ -47,8 +45,8 @@
 | "b_lrb (Clause fcs) = (b_fnclauses fcs)"
 | "b_fnclause (K x pat exp) = {atom x}"
 
-thm exp7_lrb_lrbs.eq_iff
-thm exp7_lrb_lrbs.supp
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.fv
+thm exp_fnclause_fnclauses_lrb_lrbs_pat.eq_iff
 
 end