--- a/src/HOL/Integ/Integ.ML Wed Mar 27 18:45:17 1996 +0100
+++ b/src/HOL/Integ/Integ.ML Wed Mar 27 18:46:42 1996 +0100
@@ -618,10 +618,10 @@
qed "zless_not_refl";
(* z<z ==> R *)
-bind_thm ("zless_anti_refl", (zless_not_refl RS notE));
+bind_thm ("zless_irrefl", (zless_not_refl RS notE));
goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
-by(fast_tac (HOL_cs addEs [zless_anti_refl]) 1);
+by(fast_tac (HOL_cs addEs [zless_irrefl]) 1);
qed "zless_not_refl2";
@@ -677,12 +677,12 @@
goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
by (cut_facts_tac [zless_linear] 1);
-by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
+by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1);
qed "zle_imp_zless_or_eq";
goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
by (cut_facts_tac [zless_linear] 1);
-by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
+by (fast_tac (HOL_cs addEs [zless_irrefl,zless_asym]) 1);
qed "zless_or_eq_imp_zle";
goal Integ.thy "(x <= (y::int)) = (x < y | x=y)";
@@ -705,7 +705,7 @@
goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
- fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]);
+ fast_tac (HOL_cs addEs [zless_irrefl,zless_asym])]);
qed "zle_anti_sym";
--- a/src/HOL/Lambda/Lambda.ML Wed Mar 27 18:45:17 1996 +0100
+++ b/src/HOL/Lambda/Lambda.ML Wed Mar 27 18:46:42 1996 +0100
@@ -15,13 +15,13 @@
by (rtac le_less_trans 1);
by (assume_tac 2);
by(asm_full_simp_tac (!simpset addsimps [le_def]) 1);
-by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1);
+by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
qed "lt_trans1";
goal Nat.thy "!!i. [| i < j; j < Suc(k) |] ==> i < k";
by (etac less_le_trans 1);
by(asm_full_simp_tac (!simpset addsimps [le_def]) 1);
-by(fast_tac (HOL_cs addEs [less_asym,less_anti_refl]) 1);
+by(fast_tac (HOL_cs addEs [less_asym,less_irrefl]) 1);
qed "lt_trans2";
val major::prems = goal Nat.thy
--- a/src/HOL/MiniML/Type.ML Wed Mar 27 18:45:17 1996 +0100
+++ b/src/HOL/MiniML/Type.ML Wed Mar 27 18:46:42 1996 +0100
@@ -236,7 +236,7 @@
(* new type variables do not occur freely in a type structure *)
goalw thy [new_tv_def]
"!!n. new_tv n ts ==> n~:(free_tv ts)";
-by (fast_tac (HOL_cs addEs [less_anti_refl]) 1);
+by (fast_tac (HOL_cs addEs [less_irrefl]) 1);
qed "new_tv_not_free_tv";
Addsimps [new_tv_not_free_tv];
--- a/src/HOLCF/ex/Hoare.ML Wed Mar 27 18:45:17 1996 +0100
+++ b/src/HOLCF/ex/Hoare.ML Wed Mar 27 18:46:42 1996 +0100
@@ -79,11 +79,11 @@
(strip_tac 1),
(res_inst_tac [("p","b1`(iterate m g x)")] trE 1),
(atac 2),
- (rtac (le_less_trans RS less_anti_refl) 1),
+ (rtac (le_less_trans RS less_irrefl) 1),
(atac 2),
(rtac theleast2 1),
(etac hoare_lemma6 1),
- (rtac (le_less_trans RS less_anti_refl) 1),
+ (rtac (le_less_trans RS less_irrefl) 1),
(atac 2),
(rtac theleast2 1),
(etac hoare_lemma7 1)