src/HOL/Bali/AxExample.thy
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"