isabelle: src/HOL/Modelcheck/ROOT.ML@fe09a0c5cebe (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$
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	3	Author: Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	4
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	5	Basic Modelchecker examples.
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	6	*)
e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	7
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	8
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	9	(* Mucke -- mu-calculus model checker from Karlsruhe *)
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	10
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	11	use "mucke_oracle.ML";
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	12	use_thy "MuckeSyn";
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	13
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	14	if_mucke_enabled use_thy "MuckeExample1";
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	15	if_mucke_enabled use_thy "MuckeExample2";
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	16
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	17
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	18	(* Einhoven model checker *)
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	19
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	20	use_thy "CTL";
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	21	use_thy "EindhovenSyn";
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	22
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	23	if_eindhoven_enabled use_thy "EindhovenExample";

author	wenzelm
	Thu, 19 Aug 1999 19:55:13 +0200
changeset 7295	fe09a0c5cebe
parent 6465	4086e4f2edc4
child 9000	c20d58286a51
permissions	-rw-r--r--