--- 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")
--- 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)
--- 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)