--- a/src/HOL/antisym_setup.ML Thu Jul 14 19:28:14 2005 +0200
+++ b/src/HOL/antisym_setup.ML Thu Jul 14 19:28:15 2005 +0200
@@ -1,3 +1,6 @@
+
+(* $Id$ *)
+
local
val order_antisym_conv = thm "order_antisym_conv"
@@ -13,7 +16,7 @@
val t = HOLogic.mk_Trueprop(le $ s $ r);
in case Library.find_first (prp t) prems of
NONE =>
- let val t = HOLogic.mk_Trueprop(HOLogic.not_const $ (less $ r $ s))
+ let val t = HOLogic.mk_Trueprop(HOLogic.Not $ (less $ r $ s))
in case Library.find_first (prp t) prems of
NONE => NONE
| SOME thm => SOME(mk_meta_eq(thm RS linorder_antisym_conv1))
@@ -47,4 +50,4 @@
val antisym_setup =
[Simplifier.change_simpset_of (op addsimprocs) [antisym_le,antisym_less]];
-end
\ No newline at end of file
+end