isabelle: src/HOL/Modelcheck/ROOT.ML@89891b0b596f (annotated)

3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	1	(* Title: HOL/Modelcheck/ROOT.ML
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	2	ID: $Id$
6465 4086e4f2edc4 delete old files for adding second modelchecker connection; mueller parents: 3210 diff changeset	3	Author: Olaf Mueller, Tobias Hamberger, Robert Sandner
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	4	Copyright 1997 TU Muenchen
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	5
6465 4086e4f2edc4 delete old files for adding second modelchecker connection; mueller parents: 3210 diff changeset	6	This is the ROOT file for the Modelchecker examples
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	7	*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	8
6465 4086e4f2edc4 delete old files for adding second modelchecker connection; mueller parents: 3210 diff changeset	9	use_thy"EindhovenExample";
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	10
6465 4086e4f2edc4 delete old files for adding second modelchecker connection; mueller parents: 3210 diff changeset	11	use"mucke_oracle.ML";
4086e4f2edc4 delete old files for adding second modelchecker connection; mueller parents: 3210 diff changeset	12	use_thy"MuckeExample1";
4086e4f2edc4 delete old files for adding second modelchecker connection; mueller parents: 3210 diff changeset	13	use_thy"MuckeExample2";

author	paulson
	Mon, 24 May 1999 15:53:28 +0200
changeset 6715	89891b0b596f
parent 6465	4086e4f2edc4
child 7295	fe09a0c5cebe
permissions	-rw-r--r--