src/HOL/ex/Sorting.ML
changeset 2031 03a843f0f447
parent 1465 5d7a7e439cec
child 2517 2af078382853
--- a/src/HOL/ex/Sorting.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/ex/Sorting.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -11,14 +11,14 @@
           Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons];
 
 goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x";
-by(list.induct_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (list.induct_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mset_app_distr";
 
 goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \
 \                     mset xs x";
-by(list.induct_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (list.induct_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "mset_compl_add";
 
 Addsimps [mset_app_distr, mset_compl_add];