Now Datatype.occs_in_prems prints the necessary warning ITSELF.
It is also easier to invoke and even works if the induction variable
is a parameter (rather than a free variable).
<HTML><HEAD><TITLE>HOL/Modelcheck/Readme</TITLE></HEAD><BODY>
<H3>Invoking Model Checkers in Isabelle/HOL </H3>
Authors: Olaf Müller, Jan Philipps, Robert Sandner<BR>
Copyright 1997 Technische Universität München<P>
This directory contains four theories:
<UL>
<li>MuCalculus: A formalization of the relational mu calculus using the fixed point
theory Lfp and Gfp of HOL.<P>
<li>CTL: A formulation of some CTL operators in the mu calculus.<P>
<li>MCSyn: The definition of the output syntax "Eindhoven" tailored for the the model checker due to G. Janssen from Eindhoven using
the print_mode facilities provided by Isabelle. <P>
<li>Example: A simple reachability property is formulated in the mu calculus and checked
by the model checker simply by invoking the tactic mc_tac.
</UL>
Note: The example illustrates the use of the print_mode facility even without actually using the model checker. However, if you like to see the example in full functionality, get the Eindhoven model checker from here (<A HREF="http://www4.informatik.tu-muenchen.de/~mueller/tools.html">model checker binary</A>) as a Sparc SunOS4 binary which also runs under Solaris2.x, or directly from Eindhoven (<A HREF="http://www.es.ele.tue.nl/geert/research/research_index.html">model checker sources</A>), where you get the C sources and documentation.
</BODY></HTML>