All Questions
1
question
2
votes
1
answer
173
views
How do I do for-all introduction in Isabelle?
It's pretty easy to prove something like this:
theory Scratch imports Main begin
theorem "foldl (λ x y. x) a b = a"
apply (induction b)
by auto
...
- 495