Minor tidying up.
authornipkow
Wed Jul 15 10:58:44 1998 +0200 (1998-07-15)
changeset 51447ac22e5a05d7
parent 5143 b94cd208f073
child 5145 963aff0818c2
Minor tidying up.
src/HOL/Prod.ML
src/HOL/Set.thy
src/HOL/WF_Rel.ML
     1.1 --- a/src/HOL/Prod.ML	Wed Jul 15 10:15:13 1998 +0200
     1.2 +++ b/src/HOL/Prod.ML	Wed Jul 15 10:58:44 1998 +0200
     1.3 @@ -155,9 +155,6 @@
     1.4   "(%(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"];
     1.5  Addsimps split_etas; (* pragmatic solution *)
     1.6  
     1.7 -Goal "(%(x,y,z).f(x,y,z)) = t";
     1.8 -by (simp_tac (simpset() addsimps [cond_split_eta]) 1);
     1.9 -
    1.10  qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
    1.11  	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
    1.12  
     2.1 --- a/src/HOL/Set.thy	Wed Jul 15 10:15:13 1998 +0200
     2.2 +++ b/src/HOL/Set.thy	Wed Jul 15 10:58:44 1998 +0200
     2.3 @@ -71,6 +71,8 @@
     2.4    "*Ball"       :: [pttrn, 'a set, bool] => bool      ("(3ALL _:_./ _)" [0, 0, 10] 10)
     2.5    "*Bex"        :: [pttrn, 'a set, bool] => bool      ("(3EX _:_./ _)" [0, 0, 10] 10)
     2.6  
     2.7 +  disjoint      :: 'a set => 'a set => bool
     2.8 +
     2.9  translations
    2.10    "range f"     == "f``UNIV"
    2.11    "x ~: y"      == "~ (x : y)"
    2.12 @@ -87,6 +89,7 @@
    2.13    "? x:A. P"    == "Bex A (%x. P)"
    2.14    "ALL x:A. P"  => "Ball A (%x. P)"
    2.15    "EX x:A. P"   => "Bex A (%x. P)"
    2.16 +  "disjoint A B" == "A <= Compl B"
    2.17  
    2.18  syntax ("" output)
    2.19    "_setle"      :: ['a set, 'a set] => bool           ("op <=")
     3.1 --- a/src/HOL/WF_Rel.ML	Wed Jul 15 10:15:13 1998 +0200
     3.2 +++ b/src/HOL/WF_Rel.ML	Wed Jul 15 10:58:44 1998 +0200
     3.3 @@ -107,7 +107,7 @@
     3.4  
     3.5  (*---------------------------------------------------------------------------
     3.6   * Wellfoundedness of finite acyclic relations
     3.7 - * Cannot go into WF because it needs Finite
     3.8 + * Cannot go into WF because it needs Finite.
     3.9   *---------------------------------------------------------------------------*)
    3.10  
    3.11  Goal "finite r ==> acyclic r --> wf r";
    3.12 @@ -129,6 +129,7 @@
    3.13  
    3.14  (*---------------------------------------------------------------------------
    3.15   * A relation is wellfounded iff it has no infinite descending chain
    3.16 + * Cannot go into WF because it needs type nat.
    3.17   *---------------------------------------------------------------------------*)
    3.18  
    3.19  Goalw [wf_eq_minimal RS eq_reflection]