| changeset 5518 | 654ead0ba4f7 |
| parent 5124 | 1ce3cccfacdb |
| child 5655 | afd75136b236 |
--- a/src/HOL/ex/Recdefs.ML Mon Sep 21 22:58:43 1998 +0200 +++ b/src/HOL/ex/Recdefs.ML Mon Sep 21 23:03:11 1998 +0200 @@ -9,7 +9,7 @@ Addsimps qsort.rules; -Goal "(x mem qsort (ord,l)) = (x mem l)"; +Goal "(x: set (qsort (ord,l))) = (x: set l)"; by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1); by (ALLGOALS Asm_simp_tac); by (Blast_tac 1);