src/HOLCF/IOA/meta_theory/IOA.ML

eliminate get_def;

(*  Title:      HOLCF/IOA/meta_theory/IOA.thy
    ID:         $Id$
    Author:     Olaf Mueller
    Copyright   1996,1997  TU Muenchen

The theory of I/O automata in HOLCF.
*)  


val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
  by (fast_tac (claset() addDs prems) 1);
qed "imp_conj_lemma";