src/HOL/Ord.ML
changeset 6301 08245f5a436d
parent 6157 29942d3a1818
child 6433 228237ec56e5
     1.1 --- a/src/HOL/Ord.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Ord.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -161,10 +161,10 @@
     1.4  
     1.5  Goalw [min_def]
     1.6   "P(min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))";
     1.7 -by(Simp_tac 1);
     1.8 +by (Simp_tac 1);
     1.9  qed "split_min";
    1.10  
    1.11  Goalw [max_def]
    1.12   "P(max (i::'a::linorder) j) = ((i <= j --> P(j)) & (~ i <= j --> P(i)))";
    1.13 -by(Simp_tac 1);
    1.14 +by (Simp_tac 1);
    1.15  qed "split_max";