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 http://isabelle.in.tum.de/dist/Isabelle2011/doc/ref.pdf
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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.