|
167
|
1 |
(* Title: HOL/IOA/ROOT.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow & Konrad Slind
|
|
|
4 |
Copyright 1994 TU Muenchen
|
|
|
5 |
|
|
|
6 |
This is the ROOT file for the theory of I/O-Automata.
|
|
|
7 |
The formalization is by a semantic model of I/O-Automata.
|
|
|
8 |
For details see
|
|
|
9 |
|
|
|
10 |
@unpublished{Nipkow-Slind-IOA,
|
|
|
11 |
author={Tobias Nipkow and Konrad Slind},
|
|
|
12 |
title={{I/O} Automata in {Isabelle/HOL}},
|
|
|
13 |
year=1994,
|
|
|
14 |
note={Submitted for publication}}
|
|
|
15 |
ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz
|
|
|
16 |
|
|
|
17 |
Should be executed in the subdirectory HOL.
|
|
|
18 |
*)
|
|
156
|
19 |
goals_limit := 1;
|
|
|
20 |
|
|
165
|
21 |
loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath;
|
|
156
|
22 |
use_thy "Correctness";
|