# HG changeset patch
# User urbanc
# Date 1213883246 -7200
# Node ID 75b251e9cdb7e54752a0beca4af4924f5e76185b
# Parent  ba2a00d35df1d078fced37a12ddca83741b5cc97
slightly tuned

diff -r ba2a00d35df1 -r 75b251e9cdb7 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Thu Jun 19 11:46:14 2008 +0200
+++ b/src/HOL/Nominal/Examples/SN.thy	Thu Jun 19 15:47:26 2008 +0200
@@ -180,12 +180,6 @@
 where
   SN_intro: "(\<And>t'. t \<longrightarrow>\<^isub>\<beta> t' \<Longrightarrow> SN t') \<Longrightarrow> SN t"
 
-lemma SN_elim:
-  assumes a: "SN M"
-  shows "(\<forall>M. (\<forall>N. M \<longrightarrow>\<^isub>\<beta> N \<longrightarrow> P N)\<longrightarrow> P M) \<longrightarrow> P M"
-using a
-by (induct rule: SN.SN.induct) (blast)
-
 lemma SN_preserved: 
   assumes a: "SN t1" "t1\<longrightarrow>\<^isub>\<beta> t2"
   shows "SN t2"