--- a/doc-src/Locales/Locales/Examples3.thy Mon Mar 01 17:45:19 2010 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy Mon Mar 01 21:41:35 2010 +0100
@@ -63,7 +63,7 @@
statements:
@{subgoals [display]}
This is Presburger arithmetic, which can be solved by the
- method @{text arith}. *}
+ method @{text arith}. *}
by arith+
txt {* \normalsize In order to show the equations, we put ourselves
in a situation where the lattice theorems can be used in a
--- a/doc-src/Locales/Locales/document/Examples3.tex Mon Mar 01 17:45:19 2010 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex Mon Mar 01 21:41:35 2010 +0100
@@ -141,7 +141,7 @@
\ {\isadigit{2}}{\isachardot}\ {\isasymAnd}x\ y{\isachardot}\ {\isasymexists}sup{\isasymge}x{\isachardot}\ y\ {\isasymle}\ sup\ {\isasymand}\ {\isacharparenleft}{\isasymforall}z{\isachardot}\ x\ {\isasymle}\ z\ {\isasymand}\ y\ {\isasymle}\ z\ {\isasymlongrightarrow}\ sup\ {\isasymle}\ z{\isacharparenright}%
\end{isabelle}
This is Presburger arithmetic, which can be solved by the
- method \isa{arith}.%
+ method \isa{arith}.%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Mar 01 17:45:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Mon Mar 01 21:41:35 2010 +0100
@@ -286,14 +286,14 @@
by auto
lemma graph_implies_dom:
- "mrec_graph x y \<Longrightarrow> mrec_dom x"
+ "mrec_graph x y \<Longrightarrow> mrec_dom x"
apply (induct rule:mrec_graph.induct)
apply (rule accpI)
apply (erule mrec_rel.cases)
by simp
lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
- unfolding mrec_def
+ unfolding mrec_def
by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
lemma f_di_reverse:
--- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Mar 01 17:45:19 2010 +0100
+++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy Mon Mar 01 21:41:35 2010 +0100
@@ -27,8 +27,8 @@
[simp del]: "make_llist [] = return Empty"
| "make_llist (x#xs) = do tl \<leftarrow> make_llist xs;
next \<leftarrow> Ref.new tl;
- return (Node x next)
- done"
+ return (Node x next)
+ done"
text {* define traverse using the MREC combinator *}
--- a/src/HOL/Library/Transitive_Closure_Table.thy Mon Mar 01 17:45:19 2010 +0100
+++ b/src/HOL/Library/Transitive_Closure_Table.thy Mon Mar 01 21:41:35 2010 +0100
@@ -107,25 +107,25 @@
proof (cases as)
case Nil
with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
- by auto
+ by auto
from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
- by (auto elim: rtrancl_path_appendE)
+ by (auto elim: rtrancl_path_appendE)
from xs have "length cs < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: cs less(2))+
+ by (rule less(1)) (iprover intro: cs less(2))+
next
case (Cons d ds)
with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
- by auto
+ by auto
with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
and ay: "rtrancl_path r a (bs @ a # cs) y"
- by (auto elim: rtrancl_path_appendE)
+ by (auto elim: rtrancl_path_appendE)
from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
- by (rule rtrancl_path_trans)
+ by (rule rtrancl_path_trans)
from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
then show ?thesis
- by (rule less(1)) (iprover intro: xy less(2))+
+ by (rule less(1)) (iprover intro: xy less(2))+
qed
qed
qed