# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272964942 -7200
# Node ID 3842464ee03b43281915737b465cdd9b85c377f5
# Parent  94e24da9ae7542649c8d341c31a24b3d26be63f9
Move 2 more to NewParser

diff -r 94e24da9ae75 -r 3842464ee03b Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Tue May 04 11:12:09 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy	Tue May 04 11:22:22 2010 +0200
@@ -1,5 +1,5 @@
 theory ExLetRec
-imports "../Parser"
+imports "../NewParser"
 begin
 
 
@@ -7,13 +7,11 @@
 
 atom_decl name
 
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind x in t
-| Lt a::"lts" t::"trm"   bind "bn a" in t
+| Lm x::"name" t::"trm"  bind_set x in t
+| Lt a::"lts" t::"trm"   bind "bn a" in a t
 and lts =
   Lnil
 | Lcons "name" "trm" "lts"
@@ -38,13 +36,13 @@
 
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
-  by (simp add: trm_lts.eq_iff alphas2 set_sub)
+  by (simp add: trm_lts.eq_iff alphas2 set_sub supp_at_base)
 
 lemma lets_ok:
   "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
   apply (simp add: trm_lts.eq_iff)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alphas2 fresh_star_def eqvts)
+  apply (simp_all add: alphas2 fresh_star_def eqvts supp_at_base)
   done
 
 lemma lets_ok3:
@@ -72,7 +70,7 @@
 lemma lets_ok4:
   "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
    (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
-  apply (simp add: alphas trm_lts.eq_iff)
+  apply (simp add: alphas trm_lts.eq_iff supp_at_base)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
   apply (simp add: atom_eqvt fresh_star_def)
   done
diff -r 94e24da9ae75 -r 3842464ee03b Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 04 11:12:09 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 04 11:22:22 2010 +0200
@@ -1,5 +1,5 @@
 theory Lambda
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
@@ -7,7 +7,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
+| Lam x::"name" l::"lam"  bind_set x in l
 
 thm lam.fv
 thm lam.supp
@@ -17,7 +17,7 @@
 
 section {* Strong Induction Principles*}
 
-(* 
+(*
   Old way of establishing strong induction
   principles by chosing a fresh name.
 *)