# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1289854441 0
# Node ID 73196608ec0427f6e96ad405f52347b858786873
# Parent  f0252365936ca69c8f0faba01ec3b74ba0c34549
tuned example

diff -r f0252365936c -r 73196608ec04 Nominal/Ex/Foo1.thy
--- a/Nominal/Ex/Foo1.thy	Mon Nov 15 09:52:29 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Mon Nov 15 20:54:01 2010 +0000
@@ -218,6 +218,9 @@
 apply(simp add: Abs_fresh_star)
 done
 
+thm strong_exhaust1 foo.exhaust(1)
+
+
 
 lemma strong_exhaust2:
   assumes "\<And>x y t. as = As x y t \<Longrightarrow> P"