# HG changeset patch
# User paulson
# Date 905523924 -7200
# Node ID 33fcf0e60547aab19011d0dfa13103d4061fa0ae
# Parent  41ab0f44dd8f70ba95454e025efc2d630a214108
fixed comment

diff -r 41ab0f44dd8f -r 33fcf0e60547 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Sep 11 14:09:46 1998 +0200
+++ b/src/HOL/NatDef.ML	Fri Sep 11 16:25:24 1998 +0200
@@ -2,10 +2,6 @@
     ID:         $Id$
     Author:     Tobias Nipkow, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
-
-Blast_tac proofs here can get PROOF FAILED of Ord theorems like order_refl
-and order_less_irrefl.  We do not add the "nat" versions to the basic claset
-because the type will be promoted to type class "order".
 *)
 
 Goal "mono(%X. {Zero_Rep} Un (Suc_Rep``X))";