src/HOL/Nominal/Examples/Weakening.thy
changeset 32960 69916a850301
parent 26966 071f40487734
child 62390 842917225d56
--- a/src/HOL/Nominal/Examples/Weakening.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Weakening 
   imports "../Nominal" 
 begin
@@ -180,7 +178,7 @@
     proof -
       have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
       then have "[(c,x)]\<bullet>((x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc0 fc1 
-	by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
+        by (perm_simp add: eqvts calc_atm perm_fresh_fresh ty_fresh)
       then show "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#([(c,x)]\<bullet>\<Gamma>2)" by (rule perm_boolE)
     qed
     moreover 
@@ -188,7 +186,7 @@
     proof -
       have "valid \<Gamma>2" by fact
       then show "valid ((x,T1)#([(c,x)]\<bullet>\<Gamma>2))" using fc1
-	by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
+        by (auto intro!: v2 simp add: fresh_left calc_atm eqvts)
     qed
     (* these two facts give us by induction hypothesis the following *)
     ultimately have "(x,T1)#([(c,x)]\<bullet>\<Gamma>2) \<turnstile> t : T2" using ih by simp