src/HOL/Modelcheck/ROOT.ML

qed_goal -> Goal

(*  Title:      HOL/Modelcheck/ROOT.ML
    ID:         $Id$
    Author:     Olaf Mueller, Tobias Hamberger, Robert Sandner
    Copyright   1997  TU Muenchen

This is the ROOT file for the Modelchecker examples
*)

use_thy"EindhovenExample";

use"mucke_oracle.ML";
use_thy"MuckeExample1";
use_thy"MuckeExample2";