# HG changeset patch
# User nipkow
# Date 930650301 -7200
# Node ID 36de02d1a2573af00bc85205f9196574cf049913
# Parent  60a5ee0ca81db43bb83cc47d36325bf58bddff13
Bad translation fixed.

diff -r 60a5ee0ca81d -r 36de02d1a257 src/HOL/Ord.thy
--- a/src/HOL/Ord.thy	Mon Jun 28 23:05:19 1999 +0200
+++ b/src/HOL/Ord.thy	Tue Jun 29 11:58:21 1999 +0200
@@ -66,6 +66,6 @@
  "! x<y.  P"  =>  "! x. x < y  --> P"
  "! x<=y. P"  =>  "! x. x <= y --> P"
  "? x<y.  P"  =>  "? x. x < y  & P"
- "? x<=y. P"  =>  "! x. x <= y & P"
+ "? x<=y. P"  =>  "? x. x <= y & P"
 
 end