| author | nipkow | 
| Fri, 13 Oct 2000 08:28:21 +0200 | |
| changeset 10214 | 77349ed89f45 | 
| parent 9000 | c20d58286a51 | 
| child 12218 | 6597093b77e7 | 
| 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";