diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Impl.ML --- a/IOA/example/Impl.ML Wed Nov 09 19:50:36 1994 +0100 +++ b/IOA/example/Impl.ML Wed Nov 09 19:51:09 1994 +0100 @@ -1,3 +1,11 @@ +(* Title: HOL/IOA/example/Impl.ML + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +The implementation --- Invariants +*) + val impl_ioas = [Impl.impl_def, Sender.sender_ioa_def,