changeset 6814 | d96d4977f94e |
parent 6780 | 769cea1985e4 |
child 6956 | 18c0457efd3d |
--- 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];