# HG changeset patch
# User paulson
# Date 905441683 -7200
# Node ID cc95f12ab64fe8d73de6d6d3c2dffe4976cd2893
# Parent  47d0d906b39a0c239b421f1952bb390ec01e1c19
well-formed asym rules

diff -r 47d0d906b39a -r cc95f12ab64f src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Thu Sep 10 17:34:01 1998 +0200
+++ b/src/ZF/Ordinal.ML	Thu Sep 10 17:34:43 1998 +0200
@@ -228,9 +228,12 @@
 by (blast_tac (claset() addSIs [ltI] addSEs [ltE] addIs [Ord_trans]) 1);
 qed "lt_trans";
 
-Goalw [lt_def] "[| i<j;  j<i |] ==> P";
-by (REPEAT (eresolve_tac [asm_rl, conjE, mem_asym] 1));
-qed "lt_asym";
+Goalw [lt_def] "i<j ==> ~ (j<i)";
+by (blast_tac (claset() addEs [mem_asym]) 1);
+qed "lt_not_sym";
+
+(* [| i<j;  ~P ==> j<i |] ==> P *)
+bind_thm ("lt_asym", lt_not_sym RS swap);
 
 qed_goal "lt_irrefl" Ordinal.thy "i<i ==> P"
  (fn [major]=> [ (rtac (major RS (major RS lt_asym)) 1) ]);
@@ -283,7 +286,6 @@
 AddSDs [le0D];
 Addsimps [le0_iff];
 
-(*blast_tac will NOT see lt_asym*)
 val le_cs = claset() addSIs [leCI] addSEs [leE] addEs [lt_asym];