--- 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
--- 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
--- 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";
--- 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