# HG changeset patch
# User paulson
# Date 827948802 -3600
# Node ID cb62d89b7adb6c430db24e4d99e5bd5879f536bd
# Parent  372880456b5bd03655558ce87b72e150f71db2a9
Now use _irrefl instead of _anti_refl

diff -r 372880456b5b -r cb62d89b7adb src/HOL/Integ/Integ.ML
--- 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";
 
 
diff -r 372880456b5b -r cb62d89b7adb src/HOL/Lambda/Lambda.ML
--- 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
diff -r 372880456b5b -r cb62d89b7adb src/HOL/MiniML/Type.ML
--- 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];
 
diff -r 372880456b5b -r cb62d89b7adb src/HOLCF/ex/Hoare.ML
--- 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)