Re: [isabelle] formalization of non-classical logic in hilbert style
On Fri, 11 Feb 2011, Tomáš Beránek wrote:
I will maybe ask more questions about this subject, because although I
have some basic understanding of ML, I still cannot understand the code
completely (even the simpdata.ML).
There are some (outdated) explanations in
section 9.7 "Setting up the Simplifier".
In src/Pure/simplifier.ML there is also an easy_setup function that should
give an idea how the minimal setup works.
This archive was generated by a fusion of
Pipermail (Mailman edition) and