src/HOLCF/IOA/ROOT.ML

Moved most of the Prod_Syntax - stuff to HOLogic.

(*  Title:      HOL/IOA/meta_theory/ROOT.ML
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1997  TU Muenchen

This is the ROOT file for the formalization of a semantic model of I/O-Automata.

See the README.html file for details.

Should be executed in the subdirectory HOLCF/IOA/meta_theory.
*)


goals_limit:=1;

loadpath := ["meta_theory"];

use_thy"Abstraction";
use_thy"TrivEx";
use_thy"TrivEx2";