eliminated hard tabs;
authorwenzelm
Mon Mar 01 21:41:35 2010 +0100 (2010-03-01)
changeset 354236ef9525a5727
parent 35422 e74b6f3b950c
child 35424 08c37d7bd2ad
eliminated hard tabs;
doc-src/Locales/Locales/Examples3.thy
doc-src/Locales/Locales/document/Examples3.tex
src/HOL/Imperative_HOL/Heap_Monad.thy
src/HOL/Imperative_HOL/ex/Linked_Lists.thy
src/HOL/Library/Transitive_Closure_Table.thy
     1.1 --- a/doc-src/Locales/Locales/Examples3.thy	Mon Mar 01 17:45:19 2010 +0100
     1.2 +++ b/doc-src/Locales/Locales/Examples3.thy	Mon Mar 01 21:41:35 2010 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  	statements:
     1.5  	@{subgoals [display]}
     1.6  	This is Presburger arithmetic, which can be solved by the
     1.7 -	method @{text arith}. *}
     1.8 +        method @{text arith}. *}
     1.9        by arith+
    1.10      txt {* \normalsize In order to show the equations, we put ourselves
    1.11        in a situation where the lattice theorems can be used in a
     2.1 --- a/doc-src/Locales/Locales/document/Examples3.tex	Mon Mar 01 17:45:19 2010 +0100
     2.2 +++ b/doc-src/Locales/Locales/document/Examples3.tex	Mon Mar 01 21:41:35 2010 +0100
     2.3 @@ -141,7 +141,7 @@
     2.4  \ {\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}%
     2.5  \end{isabelle}
     2.6  	This is Presburger arithmetic, which can be solved by the
     2.7 -	method \isa{arith}.%
     2.8 +        method \isa{arith}.%
     2.9  \end{isamarkuptxt}%
    2.10  \isamarkuptrue%
    2.11  \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
     3.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Mar 01 17:45:19 2010 +0100
     3.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Mar 01 21:41:35 2010 +0100
     3.3 @@ -286,14 +286,14 @@
     3.4  by auto
     3.5  
     3.6  lemma graph_implies_dom:
     3.7 -	"mrec_graph x y \<Longrightarrow> mrec_dom x"
     3.8 +  "mrec_graph x y \<Longrightarrow> mrec_dom x"
     3.9  apply (induct rule:mrec_graph.induct) 
    3.10  apply (rule accpI)
    3.11  apply (erule mrec_rel.cases)
    3.12  by simp
    3.13  
    3.14  lemma f_default: "\<not> mrec_dom (f, g, x, h) \<Longrightarrow> mrec f g x h = (Inr Exn, undefined)"
    3.15 -	unfolding mrec_def 
    3.16 +  unfolding mrec_def 
    3.17    by (rule fundef_default_value[OF mrec_sumC_def graph_implies_dom, of _ _ "(f, g, x, h)", simplified])
    3.18  
    3.19  lemma f_di_reverse: 
     4.1 --- a/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Mar 01 17:45:19 2010 +0100
     4.2 +++ b/src/HOL/Imperative_HOL/ex/Linked_Lists.thy	Mon Mar 01 21:41:35 2010 +0100
     4.3 @@ -27,8 +27,8 @@
     4.4    [simp del]: "make_llist []     = return Empty"
     4.5              | "make_llist (x#xs) = do tl   \<leftarrow> make_llist xs;
     4.6                                        next \<leftarrow> Ref.new tl;
     4.7 -	                              return (Node x next)
     4.8 -		                   done"
     4.9 +                                      return (Node x next)
    4.10 +                                   done"
    4.11  
    4.12  
    4.13  text {* define traverse using the MREC combinator *}
     5.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy	Mon Mar 01 17:45:19 2010 +0100
     5.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy	Mon Mar 01 21:41:35 2010 +0100
     5.3 @@ -107,25 +107,25 @@
     5.4      proof (cases as)
     5.5        case Nil
     5.6        with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
     5.7 -	by auto
     5.8 +        by auto
     5.9        from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
    5.10 -	by (auto elim: rtrancl_path_appendE)
    5.11 +        by (auto elim: rtrancl_path_appendE)
    5.12        from xs have "length cs < length xs" by simp
    5.13        then show ?thesis
    5.14 -	by (rule less(1)) (iprover intro: cs less(2))+
    5.15 +        by (rule less(1)) (iprover intro: cs less(2))+
    5.16      next
    5.17        case (Cons d ds)
    5.18        with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
    5.19 -	by auto
    5.20 +        by auto
    5.21        with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
    5.22          and ay: "rtrancl_path r a (bs @ a # cs) y"
    5.23 -	by (auto elim: rtrancl_path_appendE)
    5.24 +        by (auto elim: rtrancl_path_appendE)
    5.25        from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
    5.26        with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
    5.27 -	by (rule rtrancl_path_trans)
    5.28 +        by (rule rtrancl_path_trans)
    5.29        from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
    5.30        then show ?thesis
    5.31 -	by (rule less(1)) (iprover intro: xy less(2))+
    5.32 +        by (rule less(1)) (iprover intro: xy less(2))+
    5.33      qed
    5.34    qed
    5.35  qed