replaced result() by qed "sorted_insort" in last proof
authorberghofe
Mon, 20 May 1996 10:11:30 +0200
changeset 1750 817a34a54fb0
parent 1749 8968b2096011
child 1751 946efd210837
replaced result() by qed "sorted_insort" in last proof
src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Fri May 17 16:22:23 1996 +0200
+++ b/src/HOL/ex/InSort.ML	Mon May 20 10:11:30 1996 +0200
@@ -40,4 +40,5 @@
 goal InSort.thy "!!f. [| total(f); transf(f) |] ==>  sorted f (insort f xs)";
 by(list.induct_tac "xs" 1);
 by(ALLGOALS Asm_simp_tac);
-result();
+qed "sorted_insort";
+