# HG changeset patch # User wenzelm # Date 972926682 -3600 # Node ID 0d0cac129618f6125d1aa3326fce4f754fdbc9b8 # Parent bf881f5fd82ff96cf012ed0f6a5a0bf17c3adbb4 tuned; diff -r bf881f5fd82f -r 0d0cac129618 src/HOL/ex/Antiquote.thy --- a/src/HOL/ex/Antiquote.thy Mon Oct 30 18:24:20 2000 +0100 +++ b/src/HOL/ex/Antiquote.thy Mon Oct 30 18:24:42 2000 +0100 @@ -6,6 +6,8 @@ Simple quote / antiquote example. *) +header {* Antiquotations *} + theory Antiquote = Main: syntax @@ -25,12 +27,12 @@ term "EXPR (a + b + c + VAR x + VAR y + 1)" term "EXPR (VAR (f w) + VAR x)" -term "Expr (%env. env x)" (*improper*) -term "Expr (%env. f env)" -term "Expr (%env. f env + env x)" (*improper*) -term "Expr (%env. f env y z)" -term "Expr (%env. f env + g y env)" -term "Expr (%env. f env + g env y + h a env z)" +term "Expr (\env. env x)" (*improper*) +term "Expr (\env. f env)" +term "Expr (\env. f env + env x)" (*improper*) +term "Expr (\env. f env y z)" +term "Expr (\env. f env + g y env)" +term "Expr (\env. f env + g env y + h a env z)" end diff -r bf881f5fd82f -r 0d0cac129618 src/HOL/ex/MonoidGroup.thy --- a/src/HOL/ex/MonoidGroup.thy Mon Oct 30 18:24:20 2000 +0100 +++ b/src/HOL/ex/MonoidGroup.thy Mon Oct 30 18:24:42 2000 +0100 @@ -6,6 +6,8 @@ Monoids and Groups as predicates over record schemes. *) +header {* Monoids and Groups *} + theory MonoidGroup = Main: record 'a monoid_sig = diff -r bf881f5fd82f -r 0d0cac129618 src/HOL/ex/Multiquote.thy --- a/src/HOL/ex/Multiquote.thy Mon Oct 30 18:24:20 2000 +0100 +++ b/src/HOL/ex/Multiquote.thy Mon Oct 30 18:24:42 2000 +0100 @@ -7,6 +7,8 @@ generalized version of de-Bruijn representation. *) +header {* Multiple nested quotations and anti-quotations *} + theory Multiquote = Main: syntax diff -r bf881f5fd82f -r 0d0cac129618 src/HOL/ex/Records.thy --- a/src/HOL/ex/Records.thy Mon Oct 30 18:24:20 2000 +0100 +++ b/src/HOL/ex/Records.thy Mon Oct 30 18:24:42 2000 +0100 @@ -24,17 +24,17 @@ thm "point.update_defs" text {* - The set of theorems "point.simps" is added automatically to the - standard simpset, "point.iffs" is added to the claset and simpset. + The set of theorems @{thm [source] point.simps} is added + automatically to the standard simpset, @{thm [source] point.iffs} is + added to the Classical Reasoner and Simplifier context. *} text {* Record declarations define new type abbreviations: - - point = "(| x :: nat, y :: nat |)" - 'a point_scheme = "(| x :: nat, y :: nat, ... :: 'a |)" - - Extensions `...' must be in type class `more'! + @{text [display] +" point = (| x :: nat, y :: nat |) + 'a point_scheme = (| x :: nat, y :: nat, ... :: 'a |)"} + Extensions `...' must be in type class @{text more}. *} consts foo1 :: point @@ -61,7 +61,7 @@ subsubsection {* Some lemmas about records *} -text {* Basic simplifications *} +text {* Basic simplifications. *} lemma "point.make n p = (| x = n, y = p |)" by simp @@ -73,7 +73,7 @@ by simp -text {* Equality of records *} +text {* \medskip Equality of records. *} lemma "n = n' ==> p = p' ==> (| x = n, y = p |) = (| x = n', y = p' |)" -- "introduction of concrete record equality" @@ -96,7 +96,7 @@ qed -text {* Surjective pairing *} +text {* \medskip Surjective pairing *} lemma "r = (| x = x r, y = y r |)" by simp @@ -105,7 +105,10 @@ by simp -text {* Splitting quantifiers: the !!r is NECESSARY here *} +text {* + \medskip Splitting quantifiers: the @{text "!!r"} is \emph{necessary} + here! +*} lemma "!!r. r (| x := n |) (| y := m |) = r (| y := m |) (| x := n |)" proof record_split @@ -124,15 +127,16 @@ qed - -text {* Concrete records are type instances of record schemes *} +text {* + \medskip Concrete records are type instances of record schemes. +*} constdefs foo5 :: nat "foo5 == getX (| x = 1, y = 0 |)" -text {* Manipulating the `...' (more) part *} +text {* \medskip Manipulating the `...' (more) part. *} constdefs incX :: "('a::more) point_scheme => 'a point_scheme" @@ -144,8 +148,7 @@ by record_split simp qed - -text {* alternative definition *} +text {* An alternative definition. *} constdefs incX' :: "('a::more) point_scheme => 'a point_scheme" @@ -162,9 +165,9 @@ text {* The record declaration defines new type constructors: - - cpoint = (| x :: nat, y :: nat, colour :: colour |) - 'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |) + @{text [display] +" cpoint = (| x :: nat, y :: nat, colour :: colour |) + 'a cpoint_scheme = (| x :: nat, y :: nat, colour :: colour, ... :: 'a |)"} *} consts foo6 :: cpoint @@ -173,7 +176,9 @@ consts foo9 :: "(| x :: nat, y :: nat, colour :: colour, ... :: 'a |)" -text {* Functions on point schemes work for cpoints as well *} +text {* + Functions on @{text point} schemes work for @{text cpoints} as well. +*} constdefs foo10 :: nat @@ -182,7 +187,10 @@ subsubsection {* Non-coercive structural subtyping *} -text {* foo11 has type cpoint, not type point --- Great! *} +text {* + Term @{term foo11} has type @{typ cpoint}, not type @{typ point} --- + Great! +*} constdefs foo11 :: cpoint @@ -191,16 +199,18 @@ subsection {* Other features *} -text {* field names contribute to record identity *} +text {* Field names contribute to record identity. *} record point' = x' :: nat y' :: nat -text {* May not apply @{term getX} to @{term "(| x' = 2, y' = 0 |)"} *} +text {* + \noindent May not apply @{term getX} to + @{term [source] "(| x' = 2, y' = 0 |)"}. +*} - -text {* Polymorphic records *} +text {* \medskip Polymorphic records. *} record 'a point'' = point + content :: 'a diff -r bf881f5fd82f -r 0d0cac129618 src/HOL/ex/Tuple.thy --- a/src/HOL/ex/Tuple.thy Mon Oct 30 18:24:20 2000 +0100 +++ b/src/HOL/ex/Tuple.thy Mon Oct 30 18:24:42 2000 +0100 @@ -9,10 +9,12 @@ tuples in HOL, but it breaks many existing theories! *) +header {* Properly nested products *} + theory Tuple = HOL: -(** abstract syntax **) +subsection {* Abstract syntax *} typedecl unit typedecl ('a, 'b) prod @@ -25,9 +27,9 @@ "()" :: unit ("'(')") -(** concrete syntax **) +subsection {* Concrete syntax *} -(* tuple types *) +subsubsection {* Tuple types *} nonterminals tuple_type_args @@ -50,7 +52,7 @@ (type) "('a, ('b, 'cs) _tuple_type) prod" -(* tuples *) +subsubsection {* Tuples *} nonterminals tuple_args @@ -63,11 +65,10 @@ "_tuple x (_tuple_args y zs)" == "Pair x (_tuple y zs)" -(* tuple patterns *) +subsubsection {* Tuple patterns *} -(*extends pre-defined type "pttrn" syntax used in abstractions*) -nonterminals - tuple_pat_args +nonterminals tuple_pat_args + -- {* extends pre-defined type "pttrn" syntax used in abstractions *} syntax "_tuple_pat_arg" :: "pttrn => tuple_pat_args" ("_") "_tuple_pat_args" :: "pttrn => tuple_pat_args => tuple_pat_args" ("_,/ _")