# HG changeset patch
# User wenzelm
# Date 1255790079 -7200
# Node ID c9fbd4a4d39efd4b98f92841145a989a23ea5186
# Parent  1df87354c3081665ea92a93751d146e3d3b0c177
tuned;

diff -r 1df87354c308 -r c9fbd4a4d39e src/HOL/ex/Refute_Examples.thy
--- 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)"