isabelle: src/HOL/Modelcheck/ROOT.ML@c63e5220ed77 (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
17272 c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	8	time_use_thy "CTL";
c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	9
c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	10
c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	11	(* Einhoven model checker *)
c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	12
c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	13	time_use_thy "EindhovenSyn";
c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	14	if_eindhoven_enabled time_use_thy "EindhovenExample";
c63e5220ed77 converted to Isar theory format; wenzelm parents: 9000 diff changeset	15
7295 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	(* Mucke -- mu-calculus model checker from Karlsruhe *)
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	18
9000 c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	19	time_use "mucke_oracle.ML";
c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	20	time_use_thy "MuckeSyn";
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	21
9000 c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	22	if_mucke_enabled time_use_thy "MuckeExample1";
c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	23	if_mucke_enabled time_use_thy "MuckeExample2";
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	24
fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	25

author	wenzelm
	Tue, 06 Sep 2005 16:24:53 +0200
changeset 17272	c63e5220ed77
parent 9000	c20d58286a51
child 23556	c09cc406460b
permissions	-rw-r--r--