author | nipkow |
Wed, 29 Nov 2000 17:23:27 +0100 | |
changeset 10539 | 5929460a41df |
parent 9000 | c20d58286a51 |
child 17272 | c63e5220ed77 |
permissions | -rw-r--r-- |
(* Title: HOL/Modelcheck/ROOT.ML ID: $Id$ Author: Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen Basic Modelchecker examples. *) (* Mucke -- mu-calculus model checker from Karlsruhe *) time_use "mucke_oracle.ML"; time_use_thy "MuckeSyn"; if_mucke_enabled time_use_thy "MuckeExample1"; if_mucke_enabled time_use_thy "MuckeExample2"; (* Einhoven model checker *) time_use_thy "CTL"; time_use_thy "EindhovenSyn"; if_eindhoven_enabled time_use_thy "EindhovenExample";