src/HOL/ex/Intuitionistic.thy

--- a/src/HOL/ex/Intuitionistic.thy	Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Intuitionistic.thy	Wed Sep 14 22:08:08 2005 +0200
@@ -3,11 +3,11 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Higher-Order Logic: Intuitionistic predicate calculus problems
-
 Taken from FOL/ex/int.ML
 *)
 
+header {* Higher-Order Logic: Intuitionistic predicate calculus problems *}
+
 theory Intuitionistic imports Main begin