src/HOL/ex/Recdefs.ML
changeset 8415 852c63072334
parent 6451 bc943acc5fda
child 8624 69619f870939
--- a/src/HOL/ex/Recdefs.ML	Fri Mar 10 17:52:48 2000 +0100
+++ b/src/HOL/ex/Recdefs.ML	Fri Mar 10 17:53:16 2000 +0100
@@ -7,14 +7,6 @@
 Lemma statements from Konrad Slind's Web site
 *)
 
-Addsimps qsort.rules;
-
-Goal "(x: set (qsort (ord,l))) = (x: set l)";
-by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
-by Auto_tac;
-qed "qsort_mem_stable";
-
-
 (** The silly g function: example of nested recursion **)
 
 Addsimps g.rules;