equal
deleted
inserted
replaced
469 "f (\<forall>x. g x) \<Longrightarrow> True" |
469 "f (\<forall>x. g x) \<Longrightarrow> True" |
470 by smt+ |
470 by smt+ |
471 |
471 |
472 lemma True using let_rsp by smt |
472 lemma True using let_rsp by smt |
473 |
473 |
|
474 lemma "le = op \<le> \<Longrightarrow> le (3::int) 42" by smt |
|
475 |
474 lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps) |
476 lemma "map (\<lambda>i::nat. i + 1) [0, 1] = [1, 2]" by (smt map.simps) |
475 |
477 |
476 |
478 |
477 lemma "(ALL x. P x) | ~ All P" by smt |
479 lemma "(ALL x. P x) | ~ All P" by smt |
478 |
480 |