author wenzelm Mon, 01 Mar 2010 21:41:35 +0100 changeset 35423 6ef9525a5727 parent 35422 e74b6f3b950c child 35424 08c37d7bd2ad
eliminated hard tabs;
--- 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