changeset 33965 | f57c11db4ad4 |
parent 29258 | bce03c644efb |
child 35067 | af4c18c30593 |
--- a/src/HOL/Bali/AxExample.thy Fri Nov 27 08:42:34 2009 +0100 +++ b/src/HOL/Bali/AxExample.thy Fri Nov 27 08:42:50 2009 +0100 @@ -1,11 +1,12 @@ (* Title: HOL/Bali/AxExample.thy - ID: $Id$ Author: David von Oheimb *) header {* Example of a proof based on the Bali axiomatic semantics *} -theory AxExample imports AxSem Example begin +theory AxExample +imports AxSem Example +begin constdefs arr_inv :: "st \<Rightarrow> bool"