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

3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	1	(* Title: HOLCF/IOA/meta_theory/IOA.thy
3275 3f53f2c876f4 changes for release 94-8 mueller parents: 3071 diff changeset	2	ID: $Id$
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	3	Author: Olaf Mueller
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	4	Copyright 1996,1997 TU Muenchen
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	5
981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	6	The theory of I/O automata in HOLCF.
4533 05ecfa08fefa added newline at end of file oheimb parents: 3275 diff changeset	7	*)
05ecfa08fefa added newline at end of file oheimb parents: 3275 diff changeset	8
6467 863834a37769 added frontend syntax for IOA, moved trivial examples to folder ex; mueller parents: 4533 diff changeset	9
863834a37769 added frontend syntax for IOA, moved trivial examples to folder ex; mueller parents: 4533 diff changeset	10	val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
863834a37769 added frontend syntax for IOA, moved trivial examples to folder ex; mueller parents: 4533 diff changeset	11	by (fast_tac (claset() addDs prems) 1);
863834a37769 added frontend syntax for IOA, moved trivial examples to folder ex; mueller parents: 4533 diff changeset	12	qed "imp_conj_lemma";