--- a/src/HOL/ex/Refute_Examples.thy Sat Oct 17 16:33:14 2009 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Sat Oct 17 16:34:39 2009 +0200
@@ -1,11 +1,10 @@
(* Title: HOL/ex/Refute_Examples.thy
- ID: $Id$
Author: Tjark Weber
Copyright 2003-2007
+
+See HOL/Refute.thy for help.
*)
-(* See 'HOL/Refute.thy' for help. *)
-
header {* Examples for the 'refute' command *}
theory Refute_Examples imports Main
@@ -518,10 +517,6 @@
not generate certain axioms for recursion operators. Without these
axioms, refute may find spurious countermodels. *}
-(*
-ML {* reset quick_and_dirty; *}
-*)
-
text {* unit *}
lemma "P (x::unit)"