# HG changeset patch
# User paulson
# Date 907259378 -7200
# Node ID 95a92bc7a5916a460a87fd90150b1d1899a62916
# Parent  6b8dee1a6ebb8263d1cadfa24761be844e794f36
tidied

diff -r 6b8dee1a6ebb -r 95a92bc7a591 src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Thu Oct 01 18:29:25 1998 +0200
+++ b/src/HOL/ex/Primrec.ML	Thu Oct 01 18:29:38 1998 +0200
@@ -72,7 +72,7 @@
 
 (*PROPERTY A 5', monotonicity for<=*)
 Goal "j<=k ==> ack(i,j)<=ack(i,k)";
-by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
 by (blast_tac (claset() addIs [ack_less_mono2]) 1);
 qed "ack_le_mono2";
 
@@ -134,7 +134,7 @@
 
 (*PROPERTY A 7', monotonicity for<=*)
 Goal "i<=j ==> ack(i,k)<=ack(j,k)";
-by (full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (full_simp_tac (simpset() addsimps [order_le_less]) 1);
 by (blast_tac (claset() addIs [ack_less_mono1]) 1);
 qed "ack_le_mono1";