src/HOL/ex/Coherent.thy
changeset 32734 06c13b2e562e
parent 28323 8f12f7275637
child 47433 07f4bf913230
--- a/src/HOL/ex/Coherent.thy	Mon Sep 28 22:47:34 2009 +0200
+++ b/src/HOL/ex/Coherent.thy	Mon Sep 28 23:13:37 2009 +0200
@@ -1,14 +1,15 @@
-(*  Title:      HOL/ex/Coherent
-    ID:         $Id$
+(*  Title:      HOL/ex/Coherent.thy
     Author:     Stefan Berghofer, TU Muenchen
-                Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
+    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
 *)
 
-header{* Coherent Logic Problems *}
+header {* Coherent Logic Problems *}
 
-theory Coherent imports Main begin
+theory Coherent
+imports Main
+begin
 
-subsection{* Equivalence of two versions of Pappus' Axiom *}
+subsection {* Equivalence of two versions of Pappus' Axiom *}
 
 no_notation
   comp (infixl "o" 55) and