# HG changeset patch
# User wenzelm
# Date 1201555649 -3600
# Node ID 24c82bef5696c542fb24b9d22f2f202d0d13e06c
# Parent  3760d3ff4cced109633c8d859b6372e34adab093
eliminated escaped white space;

diff -r 3760d3ff4cce -r 24c82bef5696 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Mon Jan 28 22:27:27 2008 +0100
+++ b/src/HOL/Word/BinBoolList.thy	Mon Jan 28 22:27:29 2008 +0100
@@ -867,7 +867,7 @@
 lemma rbl_add_split: 
   "P (rbl_add (y # ys) (x # xs)) = 
     (ALL ws. length ws = length ys --> ws = rbl_add ys xs --> 
-    (y --> ((x --> P (False # rbl_succ ws)) & (~ x -->  P (True # ws)))) & \ 
+    (y --> ((x --> P (False # rbl_succ ws)) & (~ x -->  P (True # ws)))) &
     (~ y --> P (x # ws)))"
   apply (auto simp add: Let_def)
    apply (case_tac [!] "y")
diff -r 3760d3ff4cce -r 24c82bef5696 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Mon Jan 28 22:27:27 2008 +0100
+++ b/src/HOL/Word/WordShift.thy	Mon Jan 28 22:27:29 2008 +0100
@@ -1005,7 +1005,7 @@
   apply (fastsimp intro ! : word_eqI simp add : word_size)
   done
 
--- {* this odd result is analogous to ucast\_id, 
+-- {* this odd result is analogous to @{text "ucast_id"}, 
       result to the length given by the result type *}
 
 lemma word_cat_id: "word_cat a b = b"
@@ -1056,7 +1056,7 @@
 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
 
 lemma cat_slices:
-  "a = slice n c ==> b = slice 0 c ==> n = size b ==> \  
+  "a = slice n c ==> b = slice 0 c ==> n = size b ==>
     size a + size b >= size c ==> word_cat a b = c"
   apply safe
   apply (rule word_eqI)
diff -r 3760d3ff4cce -r 24c82bef5696 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 28 22:27:27 2008 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 28 22:27:29 2008 +0100
@@ -549,8 +549,8 @@
 subsection "Forall"
 
 
-lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x) \
-\         --> Forall Q ys"
+lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x)
+         --> Forall Q ys"
 apply (rule_tac x="ys" in Seq_induct)
 apply (simp add: Forall_def sforall_def)
 apply simp_all
@@ -646,8 +646,8 @@
 
 
 (* holds also in other direction *)
-lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys \
-\                  --> Filter P$ys = UU "
+lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys
+                  --> Filter P$ys = UU "
 apply (rule_tac x="ys" in Seq_induct)
 apply (simp add: Forall_def sforall_def)
 apply simp_all
@@ -730,8 +730,8 @@
 
 
 lemma FilterPTakewhileQnil [simp]:
-  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \
-\   ==> Filter P$(Takewhile Q$ys) = nil"
+  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |]
+   ==> Filter P$(Takewhile Q$ys) = nil"
 apply (erule ForallnPFilterPnil)
 apply (rule ForallPForallQ)
 apply (rule ForallPTakewhileP)
@@ -739,8 +739,8 @@
 done
 
 lemma FilterPTakewhileQid [simp]:
- "!! Q P. [| !!x. Q x ==> P x |] ==> \
-\            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
+ "!! Q P. [| !!x. Q x ==> P x |] ==>
+            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
 apply (rule ForallPFilterPid)
 apply (rule ForallPForallQ)
 apply (rule ForallPTakewhileP)