src/HOL/ex/Sorting.ML
changeset 3647 a64c8fbcd98f
parent 3465 e85c24717cad
child 3842 b55686a7b22c
--- a/src/HOL/ex/Sorting.ML	Sun Aug 10 12:28:34 1997 +0200
+++ b/src/HOL/ex/Sorting.ML	Thu Aug 21 12:53:23 1997 +0200
@@ -23,7 +23,7 @@
 by (list.induct_tac "xs" 1);
 by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 by (Fast_tac 1);
-qed "set_of_list_via_mset";
+qed "set_via_mset";
 
 (* Equivalence of two definitions of `sorted' *)