info
Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss
First steps: theory Scratch
27 views
Skip to first unread message
Kevin Liu
Mar 6, 2017, 4:20:45 PM3/6/17
to
Hello, I entered on Isabelle/HOL
theory Scratch
imports Main
begin
lemma “[a] = [b] =⇒ a = b”
sledgehammer
and got output "No proof state", with boxes Proof state and Auto update checked.
What went wrong? Thanks!
theory Scratch
imports Main
begin
lemma “[a] = [b] =⇒ a = b”
sledgehammer
and got output "No proof state", with boxes Proof state and Auto update checked.
What went wrong? Thanks!
0 new messages