ex/InSort.ML

--- a/ex/InSort.ML	Fri Nov 11 10:35:03 1994 +0100
+++ b/ex/InSort.ML	Mon Nov 21 17:50:34 1994 +0100
@@ -12,12 +12,12 @@
 goalw InSort.thy [Sorting.total_def]
   "!!f. [| total(f); ~f(x,y) |] ==> f(y,x)";
 by(fast_tac HOL_cs 1);
-val totalD = result();
+qed "totalD";
 
 goalw InSort.thy [Sorting.transf_def]
   "!!f. [| transf(f); f(b,a) |] ==> !x. f(a,x) --> f(b,x)";
 by(fast_tac HOL_cs 1);
-val transfD = result();
+qed "transfD";
 
 goal InSort.thy "list_all(p,ins(f,x,xs)) = (list_all(p,xs) & p(x))";
 by(list_ind_tac "xs" 1);
@@ -29,7 +29,7 @@
 goal InSort.thy "(!x. p(x) --> q(x)) --> list_all(p,xs) --> list_all(q,xs)";
 by(list_ind_tac "xs" 1);
 by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if]))));
-val list_all_imp = result();
+qed "list_all_imp";
 
 val prems = goal InSort.thy
   "[| total(f); transf(f) |] ==>  sorted(f,ins(f,x,xs)) = sorted(f,xs)";