--- a/Separation_Algebra/Separation_Algebra.thy	Fri Mar 21 21:40:51 2014 +0800
+++ b/Separation_Algebra/Separation_Algebra.thy	Fri Mar 21 13:49:20 2014 +0000
@@ -35,7 +35,7 @@
   pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where
   "\<langle>f\<rangle> \<equiv> \<lambda>s. f"
 
-(* abbreviation *)
+(* was an abbreviation *)
   definition pred_ex :: "('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" (binder "EXS " 10) where
   "EXS x. P x \<equiv> \<lambda>s. \<exists>x. P x s"
 
@@ -216,7 +216,6 @@
   then obtain x y z where "P x" and "Q y" and "R z"
                       and "x ## y" and "x ## z" and "y ## z" and "x ## y + z"
                       and "h = x + y + z"
-    thm sep_disj_addD
     by (fastforce elim!: sep_conjE simp: sep_add_ac dest: sep_disj_addD)
   thus "?lhs h"
     by (metis sep_conj_def sep_disj_addI1)