# HG changeset patch
# User nipkow
# Date 971426945 -7200
# Node ID 1ead773b365ee795c9b32af8b1204e4f25f90f29
# Parent  77349ed89f4536014e5deee466bf8f5426b4ddfb
*** empty log message ***

diff -r 77349ed89f45 -r 1ead773b365e src/HOLCF/IOA/ABP/Lemmas.thy
--- a/src/HOLCF/IOA/ABP/Lemmas.thy	Fri Oct 13 08:28:21 2000 +0200
+++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Fri Oct 13 10:49:05 2000 +0200
@@ -6,4 +6,4 @@
 Arithmetic lemmas
 *)
 
-Lemmas = Arithmetic
+Lemmas = NatArith
diff -r 77349ed89f45 -r 1ead773b365e src/HOLCF/IOA/ABP/Packet.thy
--- a/src/HOLCF/IOA/ABP/Packet.thy	Fri Oct 13 08:28:21 2000 +0200
+++ b/src/HOLCF/IOA/ABP/Packet.thy	Fri Oct 13 10:49:05 2000 +0200
@@ -6,7 +6,7 @@
 Packets
 *)
 
-Packet = Arithmetic +
+Packet = NatArith +
 
 types
 
diff -r 77349ed89f45 -r 1ead773b365e src/HOLCF/IOA/NTP/Lemmas.ML
--- a/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Oct 13 08:28:21 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Fri Oct 13 10:49:05 2000 +0200
@@ -35,7 +35,7 @@
 
 (* Arithmetic *)
 
-goal Arithmetic.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
+goal NatArith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
 by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
 qed "pred_suc";
 
diff -r 77349ed89f45 -r 1ead773b365e src/HOLCF/IOA/NTP/Lemmas.thy
--- a/src/HOLCF/IOA/NTP/Lemmas.thy	Fri Oct 13 08:28:21 2000 +0200
+++ b/src/HOLCF/IOA/NTP/Lemmas.thy	Fri Oct 13 10:49:05 2000 +0200
@@ -6,4 +6,4 @@
 Arithmetic lemmas
 *)
 
-Lemmas = Arithmetic
+Lemmas = NatArith