# HG changeset patch
# User berghofe
# Date 832579890 -7200
# Node ID 817a34a54fb01d0ed1af21fff453d1d472949e25
# Parent  8968b2096011590322a0f4fbbcfd1963fc3ea849
replaced result() by qed "sorted_insort" in last proof

diff -r 8968b2096011 -r 817a34a54fb0 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";
+