src/HOL/UNITY/Comp/AllocBase.thy
changeset 14361 ad2f5da643b4
parent 14114 e97ca1034caa
child 14738 83f1a514dcb4
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon Jan 26 10:34:02 2004 +0100
@@ -71,13 +71,13 @@
 declare setsum_cong [cong]
 
 lemma bag_of_sublist_lemma:
-     "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
-      (\\<Sum>i: A Int lessThan k. {#f i#})"
+     "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
+      (\<Sum>i: A Int lessThan k. {#f i#})"
 by (rule setsum_cong, auto)
 
 lemma bag_of_sublist:
      "bag_of (sublist l A) =  
-      (\\<Sum>i: A Int lessThan (length l). {# l!i #})"
+      (\<Sum>i: A Int lessThan (length l). {# l!i #})"
 apply (rule_tac xs = l in rev_induct, simp)
 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
                  bag_of_sublist_lemma plus_ac0)
@@ -101,7 +101,7 @@
 lemma bag_of_sublist_UN_disjoint [rule_format]:
      "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
       ==> bag_of (sublist l (UNION I A)) =   
-          (\\<Sum>i:I. bag_of (sublist l (A i)))"
+          (\<Sum>i:I. bag_of (sublist l (A i)))"
 apply (simp del: UN_simps 
             add: UN_simps [symmetric] add: bag_of_sublist)
 apply (subst setsum_UN_disjoint, auto)