isabelle: src/HOL/Modelcheck/ROOT.ML@42f2f90b51a6 (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_thy "MuckeSyn";
3210 e80db1660614 Invoking Model Checkers in Isabelle/HOL; mueller parents: diff changeset	20
9000 c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	21	if_mucke_enabled time_use_thy "MuckeExample1";
c20d58286a51 cleaned up; wenzelm parents: 7295 diff changeset	22	if_mucke_enabled time_use_thy "MuckeExample2";

author	paulson
	Wed, 04 Jul 2007 13:56:26 +0200
changeset 23563	42f2f90b51a6
parent 23556	c09cc406460b
child 28263	69eaa97e7e96
permissions	-rw-r--r--