# 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 \ mrec_dom x" + "mrec_graph x y \ mrec_dom x" apply (induct rule:mrec_graph.induct) apply (rule accpI) apply (erule mrec_rel.cases) by simp lemma f_default: "\ mrec_dom (f, g, x, h) \ 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 \ make_llist xs; next \ 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