--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Modelcheck/README.html	Fri May 16 15:29:41 1997 +0200
@@ -0,0 +1,28 @@
+<HTML><HEAD><TITLE>HOL/Modelcheck/Readme</TITLE></HEAD><BODY>
+
+<H3>Invoking Model Checkers in Isabelle/HOL </H3>
+
+Authors:     Olaf Mueller, Jan Philipps, Robert Sandner<BR>
+Copyright   1997 Technische Universit&auml;t M&uuml;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">Eindhoven Model Checker</A>). It is provided as a Sparc SunOS4 binary which also runs under Solaris2.x. 
+
+
+
+</BODY></HTML>
+
+
+