src/HOLCF/IOA/ROOT.ML
author mueller
Mon, 12 Jan 1998 17:51:32 +0100
changeset 4563 6b9a8e956af9
parent 3071 981258186b71
child 4816 64f075872f69
permissions -rw-r--r--
added abstraction files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     1
(*  Title:      HOL/IOA/meta_theory/ROOT.ML
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     2
    ID:         $Id$
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     3
    Author:     Olaf Mueller
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     4
    Copyright   1997  TU Muenchen
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     6
This is the ROOT file for the formalization of a semantic model of I/O-Automata.
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     8
See the README.html file for details.
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     9
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    10
Should be executed in the subdirectory HOLCF/IOA/meta_theory.
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    11
*)
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    12
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    13
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    14
goals_limit:=1;
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    15
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    16
loadpath := ["meta_theory"];
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    17
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    18
use_thy"IOA";
4563
6b9a8e956af9 added abstraction files;
mueller
parents: 3071
diff changeset
    19
use_thy"Abstraction";
6b9a8e956af9 added abstraction files;
mueller
parents: 3071
diff changeset
    20
use_thy"TrivEx";
6b9a8e956af9 added abstraction files;
mueller
parents: 3071
diff changeset
    21
use_thy"TrivEx2";