# HG changeset patch
# User wenzelm
# Date 1208202293 -7200
# Node ID 25c07f3878b0ea184adb3d2a9e6d16a55da73450
# Parent  147c920ed5f784f331f3d7d4f7bda73161625495
removed duplicate lemmas;

diff -r 147c920ed5f7 -r 25c07f3878b0 src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Mon Apr 14 21:44:53 2008 +0200
@@ -5244,10 +5244,6 @@
   shows "M \<longrightarrow>\<^isub>a* M'"
 using a by blast
 
-lemma a_star_refl:
-  shows "M \<longrightarrow>\<^isub>a* M"
-  by blast
-
 lemma a_starE:
   assumes a: "M \<longrightarrow>\<^isub>a* M'"
   shows "M = M' \<or> (\<exists>N. M \<longrightarrow>\<^isub>a N \<and> N \<longrightarrow>\<^isub>a* M')"
diff -r 147c920ed5f7 -r 25c07f3878b0 src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Mon Apr 14 21:44:53 2008 +0200
+++ b/src/HOL/Nominal/Examples/Height.thy	Mon Apr 14 21:44:53 2008 +0200
@@ -75,24 +75,4 @@
   then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp 
 qed
 
-theorem height_subst:
-  shows "height (e[x::=e']) \<le> ((height e) - 1) + (height e')"
-proof (nominal_induct e avoiding: x e' rule: lam.induct)
-  case (Var y)
-  have "1 \<le> height e'" by (rule height_ge_one)
-  then show "height (Var y[x::=e']) \<le> height (Var y) - 1 + height e'" by simp
-next
-  case (Lam y e1)
-  hence ih: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" by simp
-  moreover
-  have vc: "y\<sharp>x" "y\<sharp>e'" by fact+ (* usual variable convention *)
-  ultimately show "height ((Lam [y].e1)[x::=e']) \<le> height (Lam [y].e1) - 1 + height e'" by simp
-next    
-  case (App e1 e2)
-  hence ih1: "height (e1[x::=e']) \<le> ((height e1) - 1) + (height e')" 
-    and ih2: "height (e2[x::=e']) \<le> ((height e2) - 1) + (height e')" by simp_all
-  then show "height ((App e1 e2)[x::=e']) \<le> height (App e1 e2) - 1 + height e'"  by simp 
-qed
-
-
 end