| changeset 3842 | b55686a7b22c |
| parent 3724 | f33e301a89f5 |
| child 3919 | c036caebfc75 |
--- a/src/HOL/Induct/LFilter.ML Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/Induct/LFilter.ML Fri Oct 10 19:02:28 1997 +0200 @@ -178,7 +178,7 @@ (*** lfilter: simple facts by coinduction ***) -goal thy "lfilter (%x.True) l = l"; +goal thy "lfilter (%x. True) l = l"; by (res_inst_tac [("l","l")] llist_fun_equalityI 1); by (ALLGOALS Simp_tac); by (Blast_tac 1);