src/HOL/Proofs.thy
author blanchet
Fri, 31 Jan 2014 16:41:54 +0100
changeset 55214 48a347b40629
parent 52488 cd65ee49a8ba
permissions -rw-r--r--
better tracing + syntactically correct 'metis' calls

theory Proofs
imports Pure
begin

ML "Proofterm.proofs := 2"

end