| author | wenzelm |
| Sat, 29 Apr 2006 23:16:47 +0200 | |
| changeset 19505 | 0b345cf953c4 |
| parent 19360 | f47412f922ab |
| child 19764 | 372065f34795 |
| permissions | -rw-r--r-- |
(* Title: HOLCF/IOA/Modelcheck/ROOT.ML ID: $Id$ Author: Olaf Mueller and Tobias Hamberger, TU Muenchen 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";