misc tuning and modernization;
authorwenzelm
Mon Sep 28 23:13:37 2009 +0200 (2009-09-28)
changeset 3273406c13b2e562e
parent 32733 71618deaf777
child 32735 f96f3ae3a19d
misc tuning and modernization;
src/HOL/HOL.thy
src/HOL/ex/Coherent.thy
src/Tools/coherent.ML
     1.1 --- a/src/HOL/HOL.thy	Mon Sep 28 22:47:34 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 28 23:13:37 2009 +0200
     1.3 @@ -1469,7 +1469,7 @@
     1.4  subsubsection {* Coherent logic *}
     1.5  
     1.6  ML {*
     1.7 -structure Coherent = CoherentFun
     1.8 +structure Coherent = Coherent
     1.9  (
    1.10    val atomize_elimL = @{thm atomize_elimL}
    1.11    val atomize_exL = @{thm atomize_exL}
     2.1 --- a/src/HOL/ex/Coherent.thy	Mon Sep 28 22:47:34 2009 +0200
     2.2 +++ b/src/HOL/ex/Coherent.thy	Mon Sep 28 23:13:37 2009 +0200
     2.3 @@ -1,14 +1,15 @@
     2.4 -(*  Title:      HOL/ex/Coherent
     2.5 -    ID:         $Id$
     2.6 +(*  Title:      HOL/ex/Coherent.thy
     2.7      Author:     Stefan Berghofer, TU Muenchen
     2.8 -                Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
     2.9 +    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
    2.10  *)
    2.11  
    2.12 -header{* Coherent Logic Problems *}
    2.13 +header {* Coherent Logic Problems *}
    2.14  
    2.15 -theory Coherent imports Main begin
    2.16 +theory Coherent
    2.17 +imports Main
    2.18 +begin
    2.19  
    2.20 -subsection{* Equivalence of two versions of Pappus' Axiom *}
    2.21 +subsection {* Equivalence of two versions of Pappus' Axiom *}
    2.22  
    2.23  no_notation
    2.24    comp (infixl "o" 55) and
     3.1 --- a/src/Tools/coherent.ML	Mon Sep 28 22:47:34 2009 +0200
     3.2 +++ b/src/Tools/coherent.ML	Mon Sep 28 23:13:37 2009 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4    val setup: theory -> theory
     3.5  end;
     3.6  
     3.7 -functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
     3.8 +functor Coherent(Data: COHERENT_DATA) : COHERENT =
     3.9  struct
    3.10  
    3.11  (** misc tools **)