src/HOL/Hilbert_Choice.thy
changeset 12023 d982f98e0f0d
parent 11506 244a02a2968b
child 12298 b344486c33e2
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Nov 03 01:33:33 2001 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Nov 03 01:33:54 2001 +0100
     1.3 @@ -2,9 +2,9 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson
     1.6      Copyright   2001  University of Cambridge
     1.7 +*)
     1.8  
     1.9 -Hilbert's epsilon-operator and everything to do with the Axiom of Choice
    1.10 -*)
    1.11 +header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
    1.12  
    1.13  theory Hilbert_Choice = NatArith
    1.14  files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):