Theory AxExample

Up to index of Isabelle/Bali4

(*  Title:      isabelle/Bali/AxExample.thy
    ID:         $Id: AxExample.thy,v 1.3 2000/03/30 09:38:10 oheimb Exp $
    Author:     David von Oheimb
    Copyright   2000 Technische Universitaet Muenchen
*)

AxExample = AxSem + Example

theorem ax_test:

  enough_mem
  ==> tprg,{}|-{Normal (%Ys Z. True)} .test.
      {(%Ys Z. True) \<and>. (%s. tprg,s\<turnstile>catch SXcpt NP)}
    [!]