summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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