--- a/src/HOL/UNITY/AllocBase.ML Wed Oct 18 23:41:28 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.ML Wed Oct 18 23:42:18 2000 +0200
@@ -1,12 +1,9 @@
-(* Title: HOL/UNITY/AllocBase
+(* Title: HOL/UNITY/AllocBase.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Basis declarations for Chandy and Charpentier's Allocator
-
-add_path "../Induct";
-time_use_thy "AllocBase";
*)
Goal "!!f :: nat=>nat. \
@@ -42,9 +39,9 @@
by (rewtac prefix_def);
by (etac genPrefix.induct 1);
by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1);
+by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1);
by (etac order_trans 1);
-by (rtac union_upper1 1);
+by (rtac (thm "union_upper1") 1);
qed "mono_bag_of";
(** setsum **)
--- a/src/HOL/UNITY/AllocBase.thy Wed Oct 18 23:41:28 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.thy Wed Oct 18 23:42:18 2000 +0200
@@ -1,12 +1,9 @@
-(* Title: HOL/UNITY/AllocBase
+(* Title: HOL/UNITY/AllocBase.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
Common declarations for Chandy and Charpentier's Allocator
-
-add_path "../Induct";
-time_use_thy "AllocBase";
*)
AllocBase = Rename + Follows +
--- a/src/HOL/UNITY/Follows.ML Wed Oct 18 23:41:28 2000 +0200
+++ b/src/HOL/UNITY/Follows.ML Wed Oct 18 23:42:18 2000 +0200
@@ -180,7 +180,7 @@
by (dres_inst_tac [("x","f xa")] spec 1);
by (dres_inst_tac [("x","g xa")] spec 1);
by (ball_tac 1);
-by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1);
+by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1);
qed "increasing_union";
Goalw [Increasing_def, Stable_def, Constrains_def, stable_def, constrains_def]
@@ -190,13 +190,13 @@
by (dres_inst_tac [("x","f xa")] spec 1);
by (dres_inst_tac [("x","g xa")] spec 1);
by (ball_tac 1);
-by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1);
+by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1);
qed "Increasing_union";
Goal "[| F : Always {s. f' s <= f s}; F : Always {s. g' s <= g s} |] \
\ ==> F : Always {s. f' s + g' s <= f s + (g s :: ('a::order) multiset)}";
by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-by (blast_tac (claset() addIs [union_le_mono]) 1);
+by (blast_tac (claset() addIs [thm "union_le_mono"]) 1);
qed "Always_union";
(*Except the last line, IDENTICAL to the proof script for Follows_Un_lemma*)
@@ -214,7 +214,7 @@
by (etac Stable_Int 1);
by (assume_tac 1);
by (Blast_tac 1);
-by (blast_tac (claset() addIs [union_le_mono, order_trans]) 1);
+by (blast_tac (claset() addIs [thm "union_le_mono", order_trans]) 1);
qed "Follows_union_lemma";
(*The !! is there to influence to effect of permutative rewriting at the end*)
@@ -227,7 +227,7 @@
by (rtac LeadsTo_Trans 1);
by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
(*now exchange union's arguments*)
-by (simp_tac (simpset() addsimps [union_commute]) 1);
+by (simp_tac (simpset() addsimps [thm "union_commute"]) 1);
by (blast_tac (claset() addIs [Follows_union_lemma]) 1);
qed "Follows_union";
--- a/src/HOL/UNITY/Follows.thy Wed Oct 18 23:41:28 2000 +0200
+++ b/src/HOL/UNITY/Follows.thy Wed Oct 18 23:42:18 2000 +0200
@@ -4,11 +4,9 @@
Copyright 1998 University of Cambridge
The "Follows" relation of Charpentier and Sivilotte
-
-add_path "../Induct";
*)
-Follows = SubstAx + ListOrder + MultisetOrder +
+Follows = SubstAx + ListOrder + Multiset +
constdefs
--- a/src/HOL/UNITY/ROOT.ML Wed Oct 18 23:41:28 2000 +0200
+++ b/src/HOL/UNITY/ROOT.ML Wed Oct 18 23:42:18 2000 +0200
@@ -25,7 +25,6 @@
time_use_thy "PPROD";
time_use_thy "TimerArray";
-add_path "../Induct";
time_use_thy "Alloc";
time_use_thy "AllocImpl";
time_use_thy "Client";