changeset 5618 | 721671c68324 |
parent 5223 | 4cb05273f764 |
child 6141 | a6922171b396 |
--- a/src/HOL/Induct/LFilter.ML Wed Oct 07 10:30:47 1998 +0200 +++ b/src/HOL/Induct/LFilter.ML Wed Oct 07 10:31:07 1998 +0200 @@ -58,7 +58,7 @@ "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"; by (Clarify_tac 1); by (etac findRel.induct 1); -by (blast_tac (claset() addIs (findRel.intrs@prems)) 1); +by (blast_tac (claset() addIs findRel.intrs @ prems) 1); by (blast_tac (claset() addIs findRel.intrs) 1); qed "Domain_findRel_mono";