# HG changeset patch
# User wenzelm
# Date 971905338 -7200
# Node ID 4e004b548049ba172c1004b59848b7b062cff2b6
# Parent  ef384b242d0982de256e6378f025432b58087b07
use Multiset from HOL/Library;

diff -r ef384b242d09 -r 4e004b548049 src/HOL/UNITY/AllocBase.ML
--- 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 **)
diff -r ef384b242d09 -r 4e004b548049 src/HOL/UNITY/AllocBase.thy
--- 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 + 
diff -r ef384b242d09 -r 4e004b548049 src/HOL/UNITY/Follows.ML
--- 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";
 
diff -r ef384b242d09 -r 4e004b548049 src/HOL/UNITY/Follows.thy
--- 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
 
diff -r ef384b242d09 -r 4e004b548049 src/HOL/UNITY/ROOT.ML
--- 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";