--- a/src/HOL/ex/Qsort.ML Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/ex/Qsort.ML Thu Sep 26 12:47:47 1996 +0200
@@ -9,40 +9,40 @@
Addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x";
-by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
result();
goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(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]))));
Addsimps [result()];
goal Qsort.thy
"((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))";
-by(list.induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (list.induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
val alls_lemma=result();
Addsimps [alls_lemma];
goal HOL.thy "((P --> Q) & (~P --> Q)) = Q";
-by(Fast_tac 1);
+by (Fast_tac 1);
val lemma = result();
goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))";
-by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(Asm_simp_tac 1);
-by(asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1);
-by(asm_simp_tac (!simpset addsimps [lemma]) 1);
+by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (!simpset delsimps [alls_lemma, list_all_Cons])1);
+by (asm_simp_tac (!simpset addsimps [lemma]) 1);
Addsimps [result()];
goal Qsort.thy
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \
\ (Alls x:xs. Alls y:ys. le x y))";
-by(list.induct_tac "xs" 1);
-by(Asm_simp_tac 1);
-by(asm_simp_tac (!simpset delsimps [alls_lemma]) 1);
+by (list.induct_tac "xs" 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (!simpset delsimps [alls_lemma]) 1);
Addsimps [result()];
@@ -50,12 +50,12 @@
goal Qsort.thy
"!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)";
-by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(Asm_simp_tac 1);
-by(asm_full_simp_tac (!simpset addsimps []) 1);
-by(asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1);
-by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by(Fast_tac 1);
+by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
+by (Asm_simp_tac 1);
+by (asm_full_simp_tac (!simpset addsimps []) 1);
+by (asm_full_simp_tac (!simpset addsimps [list_all_mem_conv]) 1);
+by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
+by (Fast_tac 1);
result();
(* A verification based on predicate calculus rather than combinators *)
@@ -67,31 +67,31 @@
goal Qsort.thy "x mem qsort le xs = x mem xs";
-by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
-by(Fast_tac 1);
+by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (Fast_tac 1);
Addsimps [result()];
goal Qsort.thy
"sorted le (xs@ys) = (sorted le xs & sorted le ys & \
\ (!x. x mem xs --> (!y. y mem ys --> le x y)))";
-by(list.induct_tac "xs" 1);
-by(Asm_simp_tac 1);
-by(asm_simp_tac (!simpset setloop (split_tac [expand_if])
- delsimps [list_all_conj]
- addsimps [list_all_mem_conv]) 1);
-by(Fast_tac 1);
+by (list.induct_tac "xs" 1);
+by (Asm_simp_tac 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])
+ delsimps [list_all_conj]
+ addsimps [list_all_mem_conv]) 1);
+by (Fast_tac 1);
Addsimps [result()];
goal Qsort.thy
"!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)";
-by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
-by(Simp_tac 1);
-by(asm_simp_tac (!simpset setloop (split_tac [expand_if])
- delsimps [list_all_conj]
- addsimps [list_all_mem_conv]) 1);
-by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
-by(Fast_tac 1);
+by (res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
+by (Simp_tac 1);
+by (asm_simp_tac (!simpset setloop (split_tac [expand_if])
+ delsimps [list_all_conj]
+ addsimps [list_all_mem_conv]) 1);
+by (rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]);
+by (Fast_tac 1);
result();