# HG changeset patch
# User wenzelm
# Date 1267476095 -3600
# Node ID 6ef9525a57270bef94b2aed67d43d14cd5c99b46
# Parent  e74b6f3b950c30189c9bc40a5ed5b9d1a637d32e
eliminated hard tabs;

diff -r e74b6f3b950c -r 6ef9525a5727 doc-src/Locales/Locales/Examples3.thy
--- 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
diff -r e74b6f3b950c -r 6ef9525a5727 doc-src/Locales/Locales/document/Examples3.tex
--- 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%
diff -r e74b6f3b950c -r 6ef9525a5727 src/HOL/Imperative_HOL/Heap_Monad.thy
--- 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: 
diff -r e74b6f3b950c -r 6ef9525a5727 src/HOL/Imperative_HOL/ex/Linked_Lists.thy
--- 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 *}
diff -r e74b6f3b950c -r 6ef9525a5727 src/HOL/Library/Transitive_Closure_Table.thy
--- 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