diff -r f04b33ce250f -r a4dc62a46ee4 IOA/ROOT.ML --- a/IOA/ROOT.ML Tue Oct 24 14:59:17 1995 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: HOL/IOA/ROOT.ML - ID: $Id$ - Author: Tobias Nipkow & Konrad Slind - Copyright 1994 TU Muenchen - -This is the ROOT file for the theory of I/O-Automata. -The formalization is by a semantic model of I/O-Automata. -For details see - -@unpublished{Nipkow-Slind-IOA, -author={Tobias Nipkow and Konrad Slind}, -title={{I/O} Automata in {Isabelle/HOL}}, -year=1994, -note={Submitted for publication}} -ftp://ftp.informatik.tu-muenchen.de/local/lehrstuhl/nipkow/ioa.ps.gz - -Should be executed in the subdirectory HOL. -*) -goals_limit := 1; - -loadpath := "IOA/meta_theory" :: "IOA/example" :: !loadpath; -use_thy "Correctness"; - -make_chart (); (*make HTML chart*)