# HG changeset patch
# User paulson
# Date 929004619 -7200
# Node ID d96d4977f94ee5b530b5804dc06418385700246e
# Parent  bf90f86502b22c29bb0eec9ecc88aec7ea1753f0
expandshort

diff -r bf90f86502b2 -r d96d4977f94e src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Thu Jun 10 10:41:36 1999 +0200
+++ b/src/HOL/Ord.ML	Thu Jun 10 10:50:19 1999 +0200
@@ -137,12 +137,12 @@
 (** min & max **)
 
 Goalw [min_def] "min (x::'a::order) x = x";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "min_same";
 Addsimps [min_same];
 
 Goalw [max_def] "max (x::'a::order) x = x";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "max_same";
 Addsimps [max_same];
 
diff -r bf90f86502b2 -r d96d4977f94e src/HOL/WF.ML
--- a/src/HOL/WF.ML	Thu Jun 10 10:41:36 1999 +0200
+++ b/src/HOL/WF.ML	Thu Jun 10 10:50:19 1999 +0200
@@ -236,7 +236,7 @@
 qed "acyclic_converse";
 
 Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r";
-by(blast_tac (claset() addIs [trancl_mono]) 1);
+by (blast_tac (claset() addIs [trancl_mono]) 1);
 qed "acyclic_subset";
 
 (** cut **)