src/HOL/Map.ML
changeset 6301 08245f5a436d
parent 5444 ffc64812a70b
child 7958 f531589c9fc1
--- a/src/HOL/Map.ML	Wed Mar 03 11:12:29 1999 +0100
+++ b/src/HOL/Map.ML	Wed Mar 03 11:15:18 1999 +0100
@@ -120,7 +120,7 @@
 	Asm_full_simp_tac 1]);
 
 Goalw [dom_def] "dom(m++n) = dom n Un dom m";
-by(Simp_tac 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "dom_override";
 Addsimps [dom_override];