# HG changeset patch
# User urbanc
# Date 1181730122 -7200
# Node ID 513a8ee192f13929b36a0f8cdfd49f2597cbe08f
# Parent  227c51012cdb8bc2981057502416a4e953e0fd0c
added the Q_Unit rule (was missing) and adjusted the proof accordingly

diff -r 227c51012cdb -r 513a8ee192f1 src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Wed Jun 13 11:54:03 2007 +0200
+++ b/src/HOL/Nominal/Examples/Crary.thy	Wed Jun 13 12:22:02 2007 +0200
@@ -343,6 +343,7 @@
                    \<Longrightarrow>  \<Gamma> \<turnstile> App (Lam [x]. s\<^isub>1) s\<^isub>2 \<equiv> t\<^isub>1[x::=t\<^isub>2] : T\<^isub>2"
 | Q_Ext[intro]:   "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T\<^isub>1)#\<Gamma> \<turnstile> App s (Var x) \<equiv> App t (Var x) : T\<^isub>2\<rbrakk> 
                    \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : T\<^isub>1 \<rightarrow> T\<^isub>2"
+| Q_Unit[intro]:  "\<lbrakk>\<Gamma> \<turnstile> s : TUnit; \<Gamma> \<turnstile> t: TUnit\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<equiv> t : TUnit"
 
 equivariance def_equiv
 
@@ -931,6 +932,9 @@
   }
   moreover have "valid \<Gamma>'" using h2 by auto
   ultimately show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : T\<^isub>1\<rightarrow>T\<^isub>2" by auto
+next
+  case (Q_Unit \<Gamma> s t \<Gamma>' \<theta> \<theta>')  
+  then show "\<Gamma>' \<turnstile> \<theta><s> is \<theta>'<t> : TUnit" by auto
 qed