# HG changeset patch
# User nipkow
# Date 900493124 -7200
# Node ID 7ac22e5a05d75e0f0356f27ce78e98a4570e0f11
# Parent  b94cd208f0739da6349148ad6b476c87d42f6932
Minor tidying up.

diff -r b94cd208f073 -r 7ac22e5a05d7 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Jul 15 10:15:13 1998 +0200
+++ b/src/HOL/Prod.ML	Wed Jul 15 10:58:44 1998 +0200
@@ -155,9 +155,6 @@
  "(%(a,b,c,d,e). f(a,b,c,d,e)) = f","(%(a,b,c,d,e,g). f(a,b,c,d,e,g)) = f"];
 Addsimps split_etas; (* pragmatic solution *)
 
-Goal "(%(x,y,z).f(x,y,z)) = t";
-by (simp_tac (simpset() addsimps [cond_split_eta]) 1);
-
 qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
 	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
 
diff -r b94cd208f073 -r 7ac22e5a05d7 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Jul 15 10:15:13 1998 +0200
+++ b/src/HOL/Set.thy	Wed Jul 15 10:58:44 1998 +0200
@@ -71,6 +71,8 @@
   "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
 
+  disjoint      :: 'a set => 'a set => bool
+
 translations
   "range f"     == "f``UNIV"
   "x ~: y"      == "~ (x : y)"
@@ -87,6 +89,7 @@
   "? x:A. P"    == "Bex A (%x. P)"
   "ALL x:A. P"  => "Ball A (%x. P)"
   "EX x:A. P"   => "Bex A (%x. P)"
+  "disjoint A B" == "A <= Compl B"
 
 syntax ("" output)
   "_setle"      :: ['a set, 'a set] => bool           ("op <=")
diff -r b94cd208f073 -r 7ac22e5a05d7 src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Wed Jul 15 10:15:13 1998 +0200
+++ b/src/HOL/WF_Rel.ML	Wed Jul 15 10:58:44 1998 +0200
@@ -107,7 +107,7 @@
 
 (*---------------------------------------------------------------------------
  * Wellfoundedness of finite acyclic relations
- * Cannot go into WF because it needs Finite
+ * Cannot go into WF because it needs Finite.
  *---------------------------------------------------------------------------*)
 
 Goal "finite r ==> acyclic r --> wf r";
@@ -129,6 +129,7 @@
 
 (*---------------------------------------------------------------------------
  * A relation is wellfounded iff it has no infinite descending chain
+ * Cannot go into WF because it needs type nat.
  *---------------------------------------------------------------------------*)
 
 Goalw [wf_eq_minimal RS eq_reflection]