src/HOLCF/IOA/ROOT.ML
author oheimb
Tue, 21 Apr 1998 17:22:03 +0200
changeset 4816 64f075872f69
parent 4563 6b9a8e956af9
child 6217 9dac1ee185e3
permissions -rw-r--r--
simplification of explicit theory usage and merges
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
4563
6b9a8e956af9 added abstraction files;
mueller
parents: 3071
diff changeset
    18
use_thy"Abstraction";
6b9a8e956af9 added abstraction files;
mueller
parents: 3071
diff changeset
    19
use_thy"TrivEx";
6b9a8e956af9 added abstraction files;
mueller
parents: 3071
diff changeset
    20
use_thy"TrivEx2";