--- a/src/HOL/HOL.thy Mon Sep 28 22:47:34 2009 +0200
+++ b/src/HOL/HOL.thy Mon Sep 28 23:13:37 2009 +0200
@@ -1469,7 +1469,7 @@
subsubsection {* Coherent logic *}
ML {*
-structure Coherent = CoherentFun
+structure Coherent = Coherent
(
val atomize_elimL = @{thm atomize_elimL}
val atomize_exL = @{thm atomize_exL}
--- 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
--- a/src/Tools/coherent.ML Mon Sep 28 22:47:34 2009 +0200
+++ b/src/Tools/coherent.ML Mon Sep 28 23:13:37 2009 +0200
@@ -26,7 +26,7 @@
val setup: theory -> theory
end;
-functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
+functor Coherent(Data: COHERENT_DATA) : COHERENT =
struct
(** misc tools **)