isabelle: src/HOLCF/IOA/ex/ROOT.ML@813fabceec00 (annotated)

6470 f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	1	(* Title: HOL/IOA/ex/ROOT.ML
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	2	ID: $Id$
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	3	Author: Olaf Mueller
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	4	Copyright 1997 TU Muenchen
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	5
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	6	This is the ROOT file for the formalization of a semantic model of
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	7	I/O-Automata. See the README.html file for details.
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	8	*)
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	9
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	10	goals_limit := 1;
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	11
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	12
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	13	use_thy "TrivEx";
f3015fd68d66 moved this trivial example to new ex dir; mueller parents: diff changeset	14	use_thy "TrivEx2";

author	wenzelm
	Mon, 22 May 2000 11:56:55 +0200
changeset 8907	813fabceec00
parent 6470	f3015fd68d66
child 9000	c20d58286a51
permissions	-rw-r--r--