isabelle: src/HOLCF/IOA/ABP/ROOT.ML@50be659d4222 (annotated)

3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	1	(* Title: HOL/IOA/ABP/ROOT.ML
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	2	ID: $Id$
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3	Author: Olaf Mueller
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	4	Copyright 1995 TU Muenchen
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	5
4423 a129b817b58a expandshort; wenzelm parents: 3072 diff changeset	6	This is the ROOT file for the Alternating Bit Protocol performed in
a129b817b58a expandshort; wenzelm parents: 3072 diff changeset	7	I/O-Automata.
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8	*)
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	10	goals_limit := 1;
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	11
9000 c20d58286a51 cleaned up; wenzelm parents: 6217 diff changeset	12	time_use_thy "Correctness";