# HG changeset patch
# User huffman
# Date 1273604234 25200
# Node ID 909d2680e122ed82e7ef2c7b2ed5e511eafe93f5
# Parent  6a47f043d498185a2ba6c8a6f45034bf69846127
NEWS: removed theory PReal

diff -r 6a47f043d498 -r 909d2680e122 NEWS
--- a/NEWS	Tue May 11 11:40:39 2010 -0700
+++ b/NEWS	Tue May 11 11:57:14 2010 -0700
@@ -161,6 +161,9 @@
 * Theory Library/Coinductive_List has been removed -- superceded by
 AFP/thys/Coinductive.
 
+* Theory PReal, including the type "preal" and related operations, has
+been removed.  INCOMPATIBILITY.
+
 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin,
 Min, Max from theory Finite_Set.  INCOMPATIBILITY.