author | wenzelm |

Mon Mar 01 21:41:35 2010 +0100 (2010-03-01) | |

changeset 35423 | 6ef9525a5727 |

parent 35422 | e74b6f3b950c |

child 35424 | 08c37d7bd2ad |

eliminated hard tabs;

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