src/HOLCF/IOA/NTP/ROOT.ML
author berghofe
Thu, 27 Jan 2005 12:37:02 +0100
changeset 15475 fdf9434b04ea
parent 14981 e73f8140af78
child 19360 f47412f922ab
permissions -rw-r--r--
- Proofs are now hidden by default when generating documents - New syntax for referring to theorems in lists - Improvements to theory loader (relative and absolute paths)

(*  Title:      HOL/IOA/examples/NTP/ROOT.ML
    ID:         $Id$
    Author:     Tobias Nipkow & Konrad Slind

This is the ROOT file for a network transmission protocol (NTP
subdirectory), performed in the I/O automata formalization by Olaf
Müller.
*)

goals_limit := 1;

time_use_thy "Correctness";