isabelle: src/HOLCF/IOA/ABP/ROOT.ML@6a973bd43949 (annotated)

24584 01e83ffa6c54 fixed title haftmann parents: 19360 diff changeset	1	(* Title: HOLCF/IOA/ABP/ROOT.ML
19360 f47412f922ab converted Müller to Mueller to make smlnj 110.58 work kleing parents: 17240 diff changeset	2	Author: Olaf Mueller
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	3
4423 a129b817b58a expandshort; wenzelm parents: 3072 diff changeset	4	This is the ROOT file for the Alternating Bit Protocol performed in
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 26981 diff changeset	5	I/O-Automata.
261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 26981 diff changeset	6	*)
3072 a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	7
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	8	goals_limit := 1;
a31419014be5 Old ABP files now running under the IOA meta theory based on HOLCF; mueller parents: diff changeset	9
26981 0e7ba2749d70 use: explicit .ML; wenzelm parents: 24584 diff changeset	10	use "Check.ML";
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 26981 diff changeset	11	use_thys ["Correctness"];