src/HOL/Nominal/Examples/Lam_Funs.thy

--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -1,4 +1,4 @@
-(* $Id: *)
+(* $Id$ *)
 
 theory Lam_Funs
 imports Nominal
@@ -73,7 +73,7 @@
   "subst_Lam b t \<equiv> \<lambda>a _ r. Lam [a].r"
 
 abbreviation
-  subst_syn  :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900) 
+  subst_syn  :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900) where
   "t'[b::=t] \<equiv> (lam_rec (subst_Var b t) (subst_App b t) (subst_Lam b t)) t'"
 
 (* FIXME: this lemma needs to be in Nominal.thy *)
@@ -200,7 +200,7 @@
   "psubst_Lam \<theta> \<equiv> \<lambda>a _ r. Lam [a].r"
 
 abbreviation
-  psubst_lam :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900)
+  psubst_lam :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900) where
   "t[<\<theta>>] \<equiv> (lam_rec (psubst_Var \<theta>) (psubst_App \<theta>) (psubst_Lam \<theta>)) t"
 
 lemma fin_supp_psubst:
@@ -241,4 +241,4 @@
   apply(simp add: psubst_Lam_def)
 done
 
-end
\ No newline at end of file
+end