diff -r 37a6e2f55230 -r 44ff2275d44f IOA/example/Spec.thy --- a/IOA/example/Spec.thy Wed Nov 09 19:50:36 1994 +0100 +++ b/IOA/example/Spec.thy Wed Nov 09 19:51:09 1994 +0100 @@ -1,3 +1,11 @@ +(* Title: HOL/IOA/example/Spec.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +The specification of reliable transmission +*) + Spec = List + IOA + Action + consts @@ -6,13 +14,13 @@ spec_trans :: "('m action, 'm list)transition set" spec_ioa :: "('m action, 'm list)ioa" -rules +defs sig_def "spec_sig == " -trans_def "spec_trans = \ +trans_def "spec_trans == \ \ {tr. let s = fst(tr); \ \ t = snd(snd(tr)) \ \ in \