# HG changeset patch # User wenzelm # Date 939228651 -7200 # Node ID 7fab9592384fc9bc4e1087870e88077361c35ec3 # Parent 43f8d28dbc6e3e6654f1b5a160b42ba87abdf0d0 improved presentation; diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/BasicLogic.thy --- a/src/HOL/Isar_examples/BasicLogic.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/BasicLogic.thy Wed Oct 06 18:50:51 1999 +0200 @@ -9,6 +9,7 @@ theory BasicLogic = Main:; + subsection {* Some trivialities *}; text {* Just a few toy examples to get an idea of how Isabelle/Isar @@ -62,7 +63,8 @@ qed; qed; -text {* Variations of backward vs.\ forward reasoning \dots *}; + +subsection {* Variations of backward vs.\ forward reasoning \dots *}; lemma "A & B --> B & A"; proof; diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/ExprCompiler.thy --- a/src/HOL/Isar_examples/ExprCompiler.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/ExprCompiler.thy Wed Oct 06 18:50:51 1999 +0200 @@ -37,7 +37,8 @@ *}; consts - exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"; + exec :: "(('adr, 'val) instr) list + => 'val list => ('adr => 'val) => 'val list"; primrec "exec [] stack env = stack" @@ -45,7 +46,8 @@ (case instr of Const c => exec instrs (c # stack) env | Load x => exec instrs (env x # stack) env - | Apply f => exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)"; + | Apply f => exec instrs (f (hd stack) (hd (tl stack)) + # (tl (tl stack))) env)"; constdefs execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val" @@ -55,8 +57,8 @@ subsection {* Expressions *}; text {* - We introduce a simple language of expressions: variables --- - constants --- binary operations. + We introduce a simple language of expressions: variables, constants, + binary operations. *}; datatype ('adr, 'val) expr = diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/Group.thy --- a/src/HOL/Isar_examples/Group.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/Group.thy Wed Oct 06 18:50:51 1999 +0200 @@ -71,11 +71,11 @@ qed; text {* - There are only two Isar language elements for calculational proofs: - \isakeyword{also} for initial or intermediate calculational steps, - and \isakeyword{finally} for building the result of a calculation. - These constructs are not hardwired into Isabelle/Isar, but defined on - top of the basic Isar/VM interpreter. Expanding the + \bigskip There are only two Isar language elements for calculational + proofs: \isakeyword{also} for initial or intermediate calculational + steps, and \isakeyword{finally} for building the result of a + calculation. These constructs are not hardwired into Isabelle/Isar, + but defined on top of the basic Isar/VM interpreter. Expanding the \isakeyword{also} and \isakeyword{finally} derived language elements, calculations may be simulated as demonstrated below. @@ -117,7 +117,7 @@ qed; -subsection {* Groups and monoids *}; +subsection {* Groups as monoids *}; text {* Monoids are usually defined like this. diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/KnasterTarski.thy --- a/src/HOL/Isar_examples/KnasterTarski.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Wed Oct 06 18:50:51 1999 +0200 @@ -5,16 +5,20 @@ Typical textbook proof example. *) +header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}; theory KnasterTarski = Main:; + +subsection {* Prose version *}; + text {* According to the book ``Introduction to Lattices and Order'' (by B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski - fixpoint theorem is as follows (pages 93--94). Note that we have - dualized their argument, and tuned the notation a little bit. + fixpoint theorem is as follows (pages 93--94).\footnote{We have + dualized their argument, and tuned the notation a little bit.} - \paragraph{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a + \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a complete lattice and $f \colon L \to L$ an order-preserving map. Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$. @@ -27,9 +31,12 @@ \le f(a)$. *}; + +subsection {* Formal version *}; + text {* - Our proof below closely follows this presentation. Virtually all of - the prose narration has been rephrased in terms of formal Isar + Our proof below closely follows the original presentation. Virtually + all of the prose narration has been rephrased in terms of formal Isar language elements. Just as many textbook-style proofs, there is a strong bias towards forward reasoning, and little hierarchical structure. @@ -62,5 +69,4 @@ qed; qed; - end; diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/MultisetOrder.thy --- a/src/HOL/Isar_examples/MultisetOrder.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/MultisetOrder.thy Wed Oct 06 18:50:51 1999 +0200 @@ -8,10 +8,13 @@ HOL/Induct/Multiset). Pen-and-paper proof by Wilfried Buchholz. *) +header {* Wellfoundedness of multiset ordering *}; theory MultisetOrder = Multiset:; +subsection {* A technical lemma *}; + lemma less_add: "(N, M0 + {#a#}) : mult1 r ==> (EX M. (M, M0) : mult1 r & N = M + {#a#}) | (EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K)" @@ -47,12 +50,13 @@ qed; +subsection {* The key property *}; + lemma all_accessible: "wf r ==> ALL M. M : acc (mult1 r)"; proof; let ?R = "mult1 r"; let ?W = "acc ?R"; - {{; fix M M0 a; assume wf_hyp: "ALL b. (b, a) : r --> (ALL M:?W. M + {#b#} : ?W)" @@ -97,7 +101,6 @@ qed; }}; note tedious_reasoning = this; - assume wf: "wf r"; fix M; show "M : ?W"; @@ -123,11 +126,12 @@ qed; +subsection {* Main result *}; + theorem wf_mult1: "wf r ==> wf (mult1 r)"; by (rule acc_wfI, rule all_accessible); theorem wf_mult: "wf r ==> wf (mult r)"; by (unfold mult_def, rule wf_trancl, rule wf_mult1); - end; diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/MutilatedCheckerboard.thy --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Wed Oct 06 18:50:51 1999 +0200 @@ -10,10 +10,12 @@ See also HOL/Induct/Mutil for the original Isabelle tactic scripts. *) +header {* The Mutilated Checker Board Problem *}; + theory MutilatedCheckerboard = Main:; -section {* Tilings *}; +subsection {* Tilings *}; consts tiling :: "'a set set => 'a set set"; @@ -26,7 +28,8 @@ text "The union of two disjoint tilings is a tiling"; -lemma tiling_Un: "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A"; +lemma tiling_Un: + "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A"; proof; assume "t : tiling A" (is "_ : ?T"); thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t"); @@ -41,14 +44,15 @@ have hyp: "t Un u: ?T"; by (blast!); have "a <= - (t Un u)"; by (blast!); with _ hyp; have "a Un (t Un u) : ?T"; by (rule tiling.Un); - also; have "a Un (t Un u) = (a Un t) Un u"; by (simp only: Un_assoc); + also; have "a Un (t Un u) = (a Un t) Un u"; + by (simp only: Un_assoc); finally; show "... : ?T"; .; qed; qed; qed; -section {* Basic properties of below *}; +subsection {* Basic properties of below *}; constdefs below :: "nat => nat set" @@ -60,22 +64,25 @@ lemma below_0: "below 0 = {}"; by (simp add: below_def); -lemma Sigma_Suc1: "below (Suc n) Times B = ({n} Times B) Un (below n Times B)"; +lemma Sigma_Suc1: + "below (Suc n) Times B = ({n} Times B) Un (below n Times B)"; by (simp add: below_def less_Suc_eq) blast; -lemma Sigma_Suc2: "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))"; +lemma Sigma_Suc2: + "A Times below (Suc n) = (A Times {n}) Un (A Times (below n))"; by (simp add: below_def less_Suc_eq) blast; lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2; -section {* Basic properties of evnodd *}; +subsection {* Basic properties of evnodd *}; constdefs evnodd :: "(nat * nat) set => nat => (nat * nat) set" "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}"; -lemma evnodd_iff: "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"; +lemma evnodd_iff: + "(i, j): evnodd A b = ((i, j): A & (i + j) mod 2 = b)"; by (simp add: evnodd_def); lemma evnodd_subset: "evnodd A b <= A"; @@ -97,11 +104,12 @@ by (simp add: evnodd_def); lemma evnodd_insert: "evnodd (insert (i, j) C) b = - (if (i + j) mod 2 = b then insert (i, j) (evnodd C b) else evnodd C b)"; + (if (i + j) mod 2 = b + then insert (i, j) (evnodd C b) else evnodd C b)"; by (simp add: evnodd_def) blast; -section {* Dominoes *}; +subsection {* Dominoes *}; consts domino :: "(nat * nat) set set"; @@ -111,7 +119,6 @@ horiz: "{(i, j), (i, j + 1)} : domino" vertl: "{(i, j), (i + 1, j)} : domino"; - lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino" (is "?P n" is "?B n : ?T"); proof (induct n); @@ -123,7 +130,8 @@ have "?B (Suc n) = ?a Un ?B n"; by (simp add: Sigma_Suc Un_assoc); also; have "... : ?T"; proof (rule tiling.Un); - have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz); + have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; + by (rule domino.horiz); also; have "{(i, 2 * n), (i, 2 * n + 1)} = ?a"; by blast; finally; show "... : domino"; .; from hyp; show "?B n : ?T"; .; @@ -132,7 +140,8 @@ finally; show "?P (Suc n)"; .; qed; -lemma dominoes_tile_matrix: "below m Times below (2 * n) : tiling domino" +lemma dominoes_tile_matrix: + "below m Times below (2 * n) : tiling domino" (is "?P m" is "?B m : ?T"); proof (induct m); show "?P 0"; by (simp add: below_0 tiling.empty); @@ -150,8 +159,8 @@ finally; show "?P (Suc m)"; .; qed; - -lemma domino_singleton: "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}"; +lemma domino_singleton: + "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}"; proof -; assume b: "b < 2"; assume "d : domino"; @@ -173,9 +182,10 @@ qed; -section {* Tilings of dominoes *}; +subsection {* Tilings of dominoes *}; -lemma tiling_domino_finite: "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t"); +lemma tiling_domino_finite: + "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t"); proof -; assume "t : ?T"; thus "?F t"; @@ -187,7 +197,8 @@ qed; qed; -lemma tiling_domino_01: "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)" +lemma tiling_domino_01: + "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)" (is "t : ?T ==> ?P t"); proof -; assume "t : ?T"; @@ -201,7 +212,8 @@ and hyp: "card (?e t 0) = card (?e t 1)" and "a <= - t"; - have card_suc: "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"; + have card_suc: + "!!b. b < 2 ==> card (?e (a Un t) b) = Suc (card (?e t b))"; proof -; fix b; assume "b < 2"; have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton); @@ -212,7 +224,8 @@ also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp; also; have "card ... = Suc (card (?e t b))"; proof (rule card_insert_disjoint); - show "finite (?e t b)"; by (rule evnodd_finite, rule tiling_domino_finite); + show "finite (?e t b)"; + by (rule evnodd_finite, rule tiling_domino_finite); have "(i, j) : ?e a b"; by (simp!); thus "(i, j) ~: ?e t b"; by (force! dest: evnoddD); qed; @@ -221,18 +234,20 @@ qed; hence "card (?e (a Un t) 0) = Suc (card (?e t 0))"; by simp; also; from hyp; have "card (?e t 0) = card (?e t 1)"; .; - also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; by simp; + also; from card_suc; have "Suc ... = card (?e (a Un t) 1)"; + by simp; finally; show "?P (a Un t)"; .; qed; qed; -section {* Main theorem *}; +subsection {* Main theorem *}; constdefs mutilated_board :: "nat => nat => (nat * nat) set" - "mutilated_board m n == below (2 * (m + 1)) Times below (2 * (n + 1)) - - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"; + "mutilated_board m n == + below (2 * (m + 1)) Times below (2 * (n + 1)) + - {(0, 0)} - {(2 * m + 1, 2 * n + 1)}"; theorem mutil_not_tiling: "mutilated_board m n ~: tiling domino"; proof (unfold mutilated_board_def); @@ -240,13 +255,15 @@ let ?t = "below (2 * (m + 1)) Times below (2 * (n + 1))"; let ?t' = "?t - {(0, 0)}"; let ?t'' = "?t' - {(2 * m + 1, 2 * n + 1)}"; + show "?t'' ~: ?T"; proof; have t: "?t : ?T"; by (rule dominoes_tile_matrix); assume t'': "?t'' : ?T"; let ?e = evnodd; - have fin: "finite (?e ?t 0)"; by (rule evnodd_finite, rule tiling_domino_finite, rule t); + have fin: "finite (?e ?t 0)"; + by (rule evnodd_finite, rule tiling_domino_finite, rule t); note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff; have "card (?e ?t'' 0) < card (?e ?t' 0)"; @@ -261,15 +278,16 @@ also; have "... < card (?e ?t 0)"; proof -; have "(0, 0) : ?e ?t 0"; by simp; - with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; by (rule card_Diff1_less); + with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)"; + by (rule card_Diff1_less); thus ?thesis; by simp; qed; also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01); also; have "?e ?t 1 = ?e ?t'' 1"; by simp; - also; from t''; have "card ... = card (?e ?t'' 0)"; by (rule tiling_domino_01 [RS sym]); + also; from t''; have "card ... = card (?e ?t'' 0)"; + by (rule tiling_domino_01 [RS sym]); finally; show False; ..; qed; qed; - end; diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/Summation.thy --- a/src/HOL/Isar_examples/Summation.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/Summation.thy Wed Oct 06 18:50:51 1999 +0200 @@ -11,6 +11,7 @@ theory Summation = Main:; + subsection {* A summation operator *}; consts @@ -21,14 +22,16 @@ "sum f (Suc n) = f n + sum f n"; syntax - "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); + "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); translations "SUM i < k. b" == "sum (%i. b) k"; subsection {* Summation laws *}; -syntax (* FIXME binary arithmetic does not yet work here *) +(* FIXME binary arithmetic does not yet work here *) + +syntax "3" :: nat ("3") "4" :: nat ("4") "6" :: nat ("6"); @@ -65,7 +68,8 @@ finally; show "?P (Suc n)"; by simp; qed; -theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" +theorem sum_of_squares: + "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" (is "?P n" is "?S n = _"); proof (induct n); show "?P 0"; by simp; @@ -73,7 +77,8 @@ fix n; have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp; also; assume "?S n = n * (n + 1) * (2 * n + 1)"; - also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp; + also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; + by simp; finally; show "?P (Suc n)"; by simp; qed; @@ -85,7 +90,8 @@ fix n; have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp; also; assume "?S n = (n * (n + 1))^2"; - also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp; + also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; + by simp; finally; show "?P (Suc n)"; by simp; qed; diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/W_correct.thy --- a/src/HOL/Isar_examples/W_correct.thy Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/W_correct.thy Wed Oct 06 18:50:51 1999 +0200 @@ -6,22 +6,25 @@ Based upon HOL/W0 by Dieter Nazareth and Tobias Nipkow. *) +header {* Correctness of Milner's type inference algorithm~W (let-free version) *}; + theory W_correct = Main + Type:; -section "Mini ML with type inference rules"; +subsection "Mini ML with type inference rules"; datatype expr = Var nat | Abs expr | App expr expr; -text {* type inference rules *}; +text {* Type inference rules. *}; consts has_type :: "(typ list * expr * typ) set"; syntax - "@has_type" :: "[typ list, expr, typ] => bool" ("((_) |-/ (_) :: (_))" [60, 0, 60] 60); + "@has_type" :: "[typ list, expr, typ] => bool" + ("((_) |-/ (_) :: (_))" [60, 0, 60] 60); translations "a |- e :: t" == "(a,e,t) : has_type"; @@ -32,6 +35,8 @@ AppI: "[| a |- e1 :: t2 -> t1; a |- e2 :: t2 |] ==> a |- App e1 e2 :: t1"; +text {* Type assigment is close wrt.\ substitution. *}; + lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"; proof -; assume "a |- e :: t"; @@ -40,15 +45,18 @@ fix a n; assume "n < length a"; hence "n < length (map ($ s) a)"; by simp; - hence "map ($ s) a |- Var n :: map ($ s) a ! n"; by (rule has_type.VarI); + hence "map ($ s) a |- Var n :: map ($ s) a ! n"; + by (rule has_type.VarI); also; have "map ($ s) a ! n = $ s (a ! n)"; by (rule nth_map); also; have "map ($ s) a = $ s a"; by (simp only: app_subst_list); (* FIXME unfold fails!? *) finally; show "?P a (Var n) (a ! n)"; .; next; fix a e t1 t2; assume "?P (t1 # a) e t2"; - hence "$ s t1 # map ($ s) a |- e :: $ s t2"; by (simp add: app_subst_list); - hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; by (rule has_type.AbsI); + hence "$ s t1 # map ($ s) a |- e :: $ s t2"; + by (simp add: app_subst_list); + hence "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"; + by (rule has_type.AbsI); thus "?P a (Abs e) (t1 -> t2)"; by (simp add: app_subst_list); next; fix a e1 e2 t1 t2; @@ -58,7 +66,7 @@ qed; -section {* Type inference algorithm W *}; +subsection {* Type inference algorithm W *}; consts W :: "[expr, typ list, nat] => (subst * typ * nat) maybe"; @@ -76,13 +84,16 @@ Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"; +subsection {* Correctness theorem *}; + (* FIXME proper split att/mod *) ML_setup {* Addsplits [split_bind]; *}; theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a |- e :: t"; proof -; assume W_ok: "W e a n = Ok (s, t, m)"; - have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" (is "?P e"); + have "ALL a s t m n . Ok (s, t, m) = W e a n --> $ s a |- e :: t" + (is "?P e"); proof (induct e); fix n; show "?P (Var n)"; by simp; next; @@ -91,7 +102,8 @@ proof (intro allI impI); fix a s t m n; assume "Ok (s, t, m) = W (Abs e) a n"; - hence "EX t'. t = s n -> t' & Ok (s, t', m) = W e (TVar n # a) (Suc n)"; + hence "EX t'. t = s n -> t' & + Ok (s, t', m) = W e (TVar n # a) (Suc n)"; by (rule rev_mp) simp; with hyp; show "$ s a |- Abs e :: t"; by (force intro: has_type.AbsI); @@ -116,7 +128,8 @@ and W2_ok: "W e2 ($ s1 a) n1 = Ok (s2, t2, n2)"; show ?thesis; proof (rule has_type.AppI); - from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; by (simp add: subst_comp_tel o_def); + from s; have s': "$ u ($ s2 ($ s1 a)) = $s a"; + by (simp add: subst_comp_tel o_def); show "$s a |- e1 :: $ u t2 -> t"; proof -; from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1"; by blast; @@ -126,7 +139,8 @@ qed; show "$ s a |- e2 :: $ u t2"; proof -; - from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; by blast; + from hyp2 W2_ok [RS sym]; have "$ s2 ($ s1 a) |- e2 :: t2"; + by blast; hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2"; by (rule has_type_subst_closed); with s'; show ?thesis; by simp; @@ -138,5 +152,4 @@ with W_ok [RS sym]; show ?thesis; by blast; qed; - end; diff -r 43f8d28dbc6e -r 7fab9592384f src/HOL/Isar_examples/document/style.tex --- a/src/HOL/Isar_examples/document/style.tex Wed Oct 06 18:50:40 1999 +0200 +++ b/src/HOL/Isar_examples/document/style.tex Wed Oct 06 18:50:51 1999 +0200 @@ -1,9 +1,11 @@ + +%% $Id$ \documentclass[11pt,a4paper]{article} \usepackage{isabelle,pdfsetup} \renewcommand{\isamarkupheader}[1]{\section{#1}} -%\parindent 0pt \parskip 0.5ex +\parindent 0pt \parskip 0.5ex \newcommand{\name}[1]{\textsf{#1}}