isar

7Nhiệt

2Trả lời

Bằng chứng thành ngữ do mâu thuẫn trong Isabelle?

Cho đến nay tôi đã viết chứng minh bởi sự mâu thuẫn trong phong cách sau đây trong Isabelle (sử dụng một mô hình bằng Jeremy Siek): lemma "<expression>" proof - { assume "¬ <expression>"

proof isabelle isar 2013-05-18

---