src/HOL/Induct/Multiset0.ML
changeset 6301 08245f5a436d
parent 5628 15b7f12ad919
child 8935 548901d05a0e
     1.1 --- a/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:12:29 1999 +0100
     1.2 +++ b/src/HOL/Induct/Multiset0.ML	Wed Mar 03 11:15:18 1999 +0100
     1.3 @@ -7,5 +7,5 @@
     1.4  *)
     1.5  
     1.6  Goal "(%x.0) : {f. finite {x. 0 < f x}}";
     1.7 -by(Simp_tac 1);
     1.8 +by (Simp_tac 1);
     1.9  qed "multiset_witness";