changeset 168 | 44ff2275d44f |
parent 156 | fd1be45b64bf |
child 171 | 16c4ea954511 |
--- 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,