src/HOL/UNITY/Comp/AllocBase.thy
changeset 14361 ad2f5da643b4
parent 14114 e97ca1034caa
child 14738 83f1a514dcb4
     1.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Sun Jan 25 00:42:22 2004 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon Jan 26 10:34:02 2004 +0100
     1.3 @@ -71,13 +71,13 @@
     1.4  declare setsum_cong [cong]
     1.5  
     1.6  lemma bag_of_sublist_lemma:
     1.7 -     "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
     1.8 -      (\\<Sum>i: A Int lessThan k. {#f i#})"
     1.9 +     "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
    1.10 +      (\<Sum>i: A Int lessThan k. {#f i#})"
    1.11  by (rule setsum_cong, auto)
    1.12  
    1.13  lemma bag_of_sublist:
    1.14       "bag_of (sublist l A) =  
    1.15 -      (\\<Sum>i: A Int lessThan (length l). {# l!i #})"
    1.16 +      (\<Sum>i: A Int lessThan (length l). {# l!i #})"
    1.17  apply (rule_tac xs = l in rev_induct, simp)
    1.18  apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
    1.19                   bag_of_sublist_lemma plus_ac0)
    1.20 @@ -101,7 +101,7 @@
    1.21  lemma bag_of_sublist_UN_disjoint [rule_format]:
    1.22       "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
    1.23        ==> bag_of (sublist l (UNION I A)) =   
    1.24 -          (\\<Sum>i:I. bag_of (sublist l (A i)))"
    1.25 +          (\<Sum>i:I. bag_of (sublist l (A i)))"
    1.26  apply (simp del: UN_simps 
    1.27              add: UN_simps [symmetric] add: bag_of_sublist)
    1.28  apply (subst setsum_UN_disjoint, auto)