src/HOL/ex/Higher_Order_Logic.thy
changeset 26957 e3f04fdd994d
parent 23822 bfb3b1e1d766
child 36452 d37c6eed8117
--- a/src/HOL/ex/Higher_Order_Logic.thy	Sun May 18 17:03:16 2008 +0200
+++ b/src/HOL/ex/Higher_Order_Logic.thy	Sun May 18 17:03:20 2008 +0200
@@ -5,7 +5,7 @@
 
 header {* Foundations of HOL *}
 
-theory Higher_Order_Logic imports CPure begin
+theory Higher_Order_Logic imports Pure begin
 
 text {*
   The following theory development demonstrates Higher-Order Logic