author | wenzelm |
Tue, 05 Mar 2002 20:54:55 +0100 | |
changeset 13025 | 433c57d09d53 |
parent 12218 | 6597093b77e7 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
(* Title: HOLCF/IOA/Modelcheck/ROOT.ML ID: $Id$ Author: Olaf Müller and Tobias Hamberger, TU Muenchen License: GPL (GNU GENERAL PUBLIC LICENSE) Modelchecker setup for I/O automata. *) goals_limit := 1; use "../../../HOL/Modelcheck/mucke_oracle.ML"; with_path "../../../HOL/Modelcheck" time_use_thy "MuIOAOracle"; (*examples*) if_mucke_enabled time_use_thy "Cockpit"; if_mucke_enabled time_use_thy "Ring3";