src/HOL/UNITY/AllocBase.ML
changeset 10265 4e004b548049
parent 9747 043098ba5098
     1.1 --- a/src/HOL/UNITY/AllocBase.ML	Wed Oct 18 23:41:28 2000 +0200
     1.2 +++ b/src/HOL/UNITY/AllocBase.ML	Wed Oct 18 23:42:18 2000 +0200
     1.3 @@ -1,12 +1,9 @@
     1.4 -(*  Title:      HOL/UNITY/AllocBase
     1.5 +(*  Title:      HOL/UNITY/AllocBase.ML
     1.6      ID:         $Id$
     1.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   1998  University of Cambridge
     1.9  
    1.10  Basis declarations for Chandy and Charpentier's Allocator
    1.11 -
    1.12 -add_path "../Induct";
    1.13 -time_use_thy "AllocBase";
    1.14  *)
    1.15  
    1.16  Goal "!!f :: nat=>nat. \
    1.17 @@ -42,9 +39,9 @@
    1.18  by (rewtac prefix_def);
    1.19  by (etac genPrefix.induct 1);
    1.20  by Auto_tac;
    1.21 -by (asm_full_simp_tac (simpset() addsimps [union_le_mono]) 1); 
    1.22 +by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1); 
    1.23  by (etac order_trans 1); 
    1.24 -by (rtac union_upper1 1); 
    1.25 +by (rtac (thm "union_upper1") 1); 
    1.26  qed "mono_bag_of";
    1.27  
    1.28  (** setsum **)