| changeset 55465 | 0d31c0546286 |
| parent 50666 | 6f48853f08d5 |
| child 56079 | 175ac95720d4 |
--- a/src/HOL/SMT_Examples/SMT_Examples.thy Fri Feb 14 07:53:45 2014 +0100 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy Fri Feb 14 07:53:45 2014 +0100 @@ -481,7 +481,7 @@ lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt -lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps) +lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt list.map) lemma "(ALL x. P x) | ~ All P" by smt