isabelle: src/HOL/Modelcheck/ROOT.ML@ff24ac6678dd (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
9000 c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	11	time_use "mucke_oracle.ML";
c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	12	time_use_thy "MuckeSyn";
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	13
9000 c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	14	if_mucke_enabled time_use_thy "MuckeExample1";
c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	15	if_mucke_enabled time_use_thy "MuckeExample2";
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
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
9000 c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	20	time_use_thy "CTL";
c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	21	time_use_thy "EindhovenSyn";
7295 fe09a0c5cebe quite a lot of tuning an cleanup; wenzelm parents: 6465 diff changeset	22
9000 c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	23	if_eindhoven_enabled time_use_thy "EindhovenExample";

author	nipkow
	Wed, 22 Nov 2000 13:16:55 +0100
changeset 10509	ff24ac6678dd
parent 9000	c20d58286a51
child 17272	c63e5220ed77
permissions	-rw-r--r--