# HG changeset patch
# User webertj
# Date 1100799969 -3600
# Node ID 0aff5d91242258a515817707119dbf635c2ae9e5
# Parent  36fb400f67275ba17fd99195e6e7af2190e3045d
imports (new syntax for theory headers)

diff -r 36fb400f6727 -r 0aff5d912422 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Nov 18 14:02:29 2004 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Nov 18 18:46:09 2004 +0100
@@ -8,7 +8,9 @@
 
 header {* Examples for the 'refute' command *}
 
-theory Refute_Examples = Main:
+theory Refute_Examples imports Main
+
+begin
 
 lemma "P x"
   refute