diff -r 77daf1b85cf0 -r a5f5b9336007 Separation_Algebra/Separation_Algebra.thy
--- a/Separation_Algebra/Separation_Algebra.thy	Fri Sep 12 00:47:15 2014 +0800
+++ b/Separation_Algebra/Separation_Algebra.thy	Sat Sep 13 10:07:14 2014 +0800
@@ -35,7 +35,7 @@
   pred_K :: "'b \<Rightarrow> 'a \<Rightarrow> 'b" ("\<langle>_\<rangle>") where
   "\<langle>f\<rangle> \<equiv> \<lambda>s. f"
 
-(* was an abbreviation *)
+(* 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,6 +216,7 @@
   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)