Re: [isabelle] SMT integration to Isabelle/HOL
On Mon, 16 Apr 2012, Shuling Wang wrote:
I find that our use of Isabelle/HOL needs to go to the ML level, e.g.,
defining tactics, and SMT integration mentioned above. But it is very
difficult for me to understand the ML implemental theories of
The ML tools of Isabelle/HOL are indeed quite complex, but this does not
mean that one should be afraid of Isabelle/ML in general. Isabelle/Isar
and Isabelle/ML are tightly integrated, and I usually do not speak of a
separate "ML level". It is more like the Yin and Yang (阴阳) of Isabelle.
Can you please give me some directions to learn them, or any documents
especially about the oracle and tactics faculties of Isabelle?
The isar-ref manual section 5.11 explains oracles and points to some basic
example in ~~/src/HOL/ex/Iff_Oracle.thy which can be taken as a starting
point to warm-up with Isabelle/ML and Isabelle/Isar intermixed.
This is best used with the Isabelle/jEdit Prover IDE. I.e. you start
"isabelle jedit" and open the Iff_Oracle.thy file. ML that is directly
embedded into theory sources is marked up with inferred type information
and hyperlinks for identifiers in the ML text. This greatly helps to
navigate ML sources, but it does not work yet for external ML files.
This archive was generated by a fusion of
Pipermail (Mailman edition) and