# HG changeset patch # User Christian Urban # Date 1235054693 0 # Node ID fcc0e6e54dca87dd49b33c308bb7acd416ac524a # Parent 748d9c1a32fb6dc1ef3bdd07b63f84b0ef79a4ba polished diff -r 748d9c1a32fb -r fcc0e6e54dca CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Thu Feb 19 01:09:16 2009 +0000 +++ b/CookBook/FirstSteps.thy Thu Feb 19 14:44:53 2009 +0000 @@ -62,7 +62,7 @@ *} -section {* Debugging and Printing *} +section {* Debugging and Printing\label{sec:printing} *} text {* @@ -118,9 +118,230 @@ "Exception- ERROR \"foo\" raised At command \"ML\"."} - Section~\ref{sec:printing} will give more information about printing - the main data structures of Isabelle, namely @{ML_type term}, @{ML_type cterm} - and @{ML_type thm}. + Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} + or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, + but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform + a term into a string is to use the function @{ML Syntax.string_of_term}. + + @{ML_response_fake [display,gray] + "Syntax.string_of_term @{context} @{term \"1::nat\"}" + "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} + + This produces a string with some additional information encoded in it. The string + can be properly printed by using the function @{ML warning}. + + @{ML_response_fake [display,gray] + "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})" + "\"1\""} + + A @{ML_type cterm} can be transformed into a string by the following function. +*} + +ML{*fun str_of_cterm ctxt t = + Syntax.string_of_term ctxt (term_of t)*} + +text {* + If there are more than one @{ML_type cterm}s to be printed, you can use the + function @{ML commas} to separate them. +*} + +ML{*fun str_of_cterms ctxt ts = + commas (map (str_of_cterm ctxt) ts)*} + +text {* + The easiest way to get the string of a theorem is to transform it + into a @{ML_type cterm} using the function @{ML crep_thm}. +*} + +ML{*fun str_of_thm ctxt thm = + let + val {prop, ...} = crep_thm thm + in + str_of_cterm ctxt prop + end*} + +text {* + Again the function @{ML commas} helps with printing more than one theorem. +*} + +ML{*fun str_of_thms ctxt thms = + commas (map (str_of_thm ctxt) thms)*} + + +section {* Combinators\label{sec:combinators} *} + +text {* + (FIXME: maybe move before antiquotation section) + + For beginners, perhaps the most puzzling parts in the existing code of Isabelle are + the combinators. At first they seem to greatly obstruct the + comprehension of the code, but after getting familiar with them, they + actually ease the understanding and also the programming. + + \begin{readmore} + The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} + and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} + contains further information about combinators. + \end{readmore} + + The simplest combinator is @{ML I}, which is just the identity function defined as +*} + +ML{*fun I x = x*} + +text {* Another simple combinator is @{ML K}, defined as *} + +ML{*fun K x = fn _ => x*} + +text {* + @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this + function ignores its argument. As a result, @{ML K} defines a constant function + always returning @{text x}. + + The next combinator is reverse application, @{ML "|>"}, defined as: +*} + +ML{*fun x |> f = f x*} + +text {* While just syntactic sugar for the usual function application, + the purpose of this combinator is to implement functions in a + ``waterfall fashion''. Consider for example the function *} + +ML %linenosgray{*fun inc_by_five x = + x |> (fn x => x + 1) + |> (fn x => (x, x)) + |> fst + |> (fn x => x + 4)*} + +text {* + which increments its argument @{text x} by 5. It does this by first incrementing + the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking + the first component of the pair (Line 4) and finally incrementing the first + component by 4 (Line 5). This kind of cascading manipulations of values is quite + common when dealing with theories (for example by adding a definition, followed by + lemmas and so on). The reverse application allows you to read what happens in + a top-down manner. This kind of coding should also be familiar, + if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using + the reverse application is much clearer than writing +*} + +ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*} + +text {* or *} + +ML{*fun inc_by_five x = + ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*} + +text {* and typographically more economical than *} + +ML{*fun inc_by_five x = + let val y1 = x + 1 + val y2 = (y1, y1) + val y3 = fst y2 + val y4 = y3 + 4 + in y4 end*} + +text {* + Another reason why the let-bindings in the code above are better to be + avoided: it is more than easy to get the intermediate values wrong, not to + mention the nightmares the maintenance of this code causes! + + + (FIXME: give a real world example involving theories) + + Similarly, the combinator @{ML "#>"} is the reverse function + composition. It can be used to define the following function +*} + +ML{*val inc_by_six = + (fn x => x + 1) + #> (fn x => x + 2) + #> (fn x => x + 3)*} + +text {* + which is the function composed of first the increment-by-one function and then + increment-by-two, followed by increment-by-three. Again, the reverse function + composition allows you to read the code top-down. + + The remaining combinators described in this section add convenience for the + ``waterfall method'' of writing functions. The combinator @{ML tap} allows + you to get hold of an intermediate result (to do some side-calculations for + instance). The function + + *} + +ML %linenosgray{*fun inc_by_three x = + x |> (fn x => x + 1) + |> tap (fn x => tracing (makestring x)) + |> (fn x => x + 2)*} + +text {* + increments the argument first by @{text "1"} and then by @{text "2"}. In the + middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one'' + intermediate result inside the tracing buffer. The function @{ML tap} can + only be used for side-calculations, because any value that is computed + cannot be merged back into the ``main waterfall''. To do this, you can use + the next combinator. + + The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value + and returns the result together with the value (as a pair). For example + the function +*} + +ML{*fun inc_as_pair x = + x |> `(fn x => x + 1) + |> (fn (x, y) => (x, y + 1))*} + +text {* + takes @{text x} as argument, and then increments @{text x}, but also keeps + @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)" + for x}. After that, the function increments the right-hand component of the + pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}. + + The combinators @{ML "|>>"} and @{ML "||>"} are defined for + functions manipulating pairs. The first applies the function to + the first component of the pair, defined as +*} + +ML{*fun (x, y) |>> f = (f x, y)*} + +text {* + and the second combinator to the second component, defined as +*} + +ML{*fun (x, y) ||> f = (x, f y)*} + +text {* + With the combinator @{ML "|->"} you can re-combine the elements from a pair. + This combinator is defined as +*} + +ML{*fun (x, y) |-> f = f x y*} + +text {* and can be used to write the following roundabout version + of the @{text double} function: +*} + +ML{*fun double x = + x |> (fn x => (x, x)) + |-> (fn x => fn y => x + y)*} + +text {* + Recall that @{ML "|>"} is the reverse function applications. Recall also that the related + reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, + @{ML "|>>"} and @{ML "||>"} described above have related combinators for function + composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, + for example, the function @{text double} can also be written as: +*} + +ML{*val double = + (fn x => (x, x)) + #-> (fn x => fn y => x + y)*} + +text {* + + (FIXME: find a good exercise for combinators) + *} @@ -212,7 +433,7 @@ @{ML_response [display,gray] "@{term \"(a::nat) + b = c\"}" "Const (\"op =\", \) $ - (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} + (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} This will show the term @{term "(a::nat) + b = c"}, but printed using the internal representation of this term. This internal representation corresponds to the @@ -256,8 +477,9 @@ inserting the invisible @{text "Trueprop"}-coercions whenever necessary. Consider for example the pairs - @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" "(Free (\"P\", \) $ Free (\"x\", \), - Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} +@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" +"(Free (\"P\", \) $ Free (\"x\", \), + Const (\"Trueprop\", \) $ (Free (\"P\", \) $ Free (\"x\", \)))"} where a coercion is inserted in the second component and @@ -445,7 +667,7 @@ and @{text "(op *)"}: @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})" - "(Const (\"HOL.zero_class.zero\", \), + "(Const (\"HOL.zero_class.zero\", \), Const (\"HOL.times_class.times\", \))"} While you could use the complete name, for example @@ -471,7 +693,7 @@ @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""} The difference between both functions is that @{ML extern_const in Sign} returns - the smallest name which is still unique, while @{ML base_name in Sign} always + the smallest name that is still unique, whereas @{ML base_name in Sign} always strips off all qualifiers. (FIXME authentic syntax on the ML-level) @@ -567,13 +789,14 @@ @{ML_response_fake [display,gray] "let - val term = - Const (@{const_name \"plus\"}, dummyT) $ @{term \"1::nat\"} $ Free (\"x\", dummyT) + val c = Const (@{const_name \"plus\"}, dummyT) + val o = @{term \"1::nat\"} + val v = Free (\"x\", dummyT) in - Syntax.check_term @{context} term + Syntax.check_term @{context} (c $ o $ v) end" - "Const (\"HOL.plus_class.plus\", \"nat \ nat \ nat\") $ - Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} +"Const (\"HOL.plus_class.plus\", \"nat \ nat \ nat\") $ + Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"} Instead of giving explicitly the type for the constant @{text "plus"} and the free variable @{text "x"}, the type-inference will fill in the missing information. @@ -654,240 +877,36 @@ (FIXME: how to add case-names to goal states) *} -section {* Printing Terms and Theorems\label{sec:printing} *} - -text {* - During development, you often want to inspect date of type @{ML_type term}, @{ML_type cterm} - or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them, - but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform - a term into a string is to use the function @{ML Syntax.string_of_term}. - - @{ML_response_fake [display,gray] - "Syntax.string_of_term @{context} @{term \"1::nat\"}" - "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} - - This produces a string with some printing directions encoded in it. The string - can be properly printed by using the function @{ML warning}. - - @{ML_response_fake [display,gray] - "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})" - "\"1\""} - - A @{ML_type cterm} can be transformed into a string by the following function. -*} - -ML{*fun str_of_cterm ctxt t = - Syntax.string_of_term ctxt (term_of t)*} - -text {* - If there are more than one @{ML_type cterm}s to be printed, you can use the - function @{ML commas} to separate them. -*} - -ML{*fun str_of_cterms ctxt ts = - commas (map (str_of_cterm ctxt) ts)*} - -text {* - The easiest way to get the string of a theorem is to transform it - into a @{ML_type cterm} using the function @{ML crep_thm}. -*} - -ML{*fun str_of_thm ctxt thm = - let - val {prop, ...} = crep_thm thm - in - str_of_cterm ctxt prop - end*} - -text {* - Again the function @{ML commas} helps with printing more than one theorem. -*} - -ML{*fun str_of_thms ctxt thms = - commas (map (str_of_thm ctxt) thms)*} section {* Theorem Attributes *} section {* Theories and Local Theories *} +text {* + (FIXME: expand) + + There are theories, proof contexts and local theories (in this order, if you + want to order them). + + In contrast to an ordinary theory, which simply consists of a type + signature, as well as tables for constants, axioms and theorems, a local + theory also contains additional context information, such as locally fixed + variables and local assumptions that may be used by the package. The type + @{ML_type local_theory} is identical to the type of \emph{proof contexts} + @{ML_type "Proof.context"}, although not every proof context constitutes a + valid local theory. + + *} + + + section {* Storing Theorems *} text {* @{ML PureThy.add_thms_dynamic} *} -section {* Combinators\label{sec:combinators} *} -text {* - For beginners, perhaps the most puzzling parts in the existing code of Isabelle are - the combinators. At first they seem to greatly obstruct the - comprehension of the code, but after getting familiar with them, they - actually ease the understanding and also the programming. - - \begin{readmore} - The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} - and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} - contains further information about combinators. - \end{readmore} - - The simplest combinator is @{ML I}, which is just the identity function defined as -*} - -ML{*fun I x = x*} - -text {* Another simple combinator is @{ML K}, defined as *} - -ML{*fun K x = fn _ => x*} - -text {* - @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this - function ignores its argument. As a result, @{ML K} defines a constant function - always returning @{text x}. - - The next combinator is reverse application, @{ML "|>"}, defined as: -*} - -ML{*fun x |> f = f x*} - -text {* While just syntactic sugar for the usual function application, - the purpose of this combinator is to implement functions in a - ``waterfall fashion''. Consider for example the function *} - -ML %linenosgray{*fun inc_by_five x = - x |> (fn x => x + 1) - |> (fn x => (x, x)) - |> fst - |> (fn x => x + 4)*} - -text {* - which increments its argument @{text x} by 5. It does this by first incrementing - the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking - the first component of the pair (Line 4) and finally incrementing the first - component by 4 (Line 5). This kind of cascading manipulations of values is quite - common when dealing with theories (for example by adding a definition, followed by - lemmas and so on). The reverse application allows you to read what happens in - a top-down manner. This kind of coding should also be familiar, - if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using - the reverse application is much clearer than writing -*} - -ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*} - -text {* or *} - -ML{*fun inc_by_five x = - ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*} - -text {* and typographically more economical than *} - -ML{*fun inc_by_five x = - let val y1 = x + 1 - val y2 = (y1, y1) - val y3 = fst y2 - val y4 = y3 + 4 - in y4 end*} - -text {* - Another reason why the let-bindings in the code above are better to be - avoided: it is more than easy to get the intermediate values wrong, not to - mention the nightmares the maintenance of this code causes! - - - (FIXME: give a real world example involving theories) - - Similarly, the combinator @{ML "#>"} is the reverse function - composition. It can be used to define the following function -*} - -ML{*val inc_by_six = - (fn x => x + 1) - #> (fn x => x + 2) - #> (fn x => x + 3)*} - -text {* - which is the function composed of first the increment-by-one function and then - increment-by-two, followed by increment-by-three. Again, the reverse function - composition allows you to read the code top-down. - - The remaining combinators described in this section add convenience for the - ``waterfall method'' of writing functions. The combinator @{ML tap} allows - you to get hold of an intermediate result (to do some side-calculations for - instance). The function - - *} - -ML %linenosgray{*fun inc_by_three x = - x |> (fn x => x + 1) - |> tap (fn x => tracing (makestring x)) - |> (fn x => x + 2)*} - -text {* - increments the argument first by @{text "1"} and then by @{text "2"}. In the - middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one'' - intermediate result inside the tracing buffer. The function @{ML tap} can - only be used for side-calculations, because any value that is computed - cannot be merged back into the ``main waterfall''. To do this, you can use - the next combinator. - - The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value - and returns the result together with the value (as a pair). For example - the function -*} - -ML{*fun inc_as_pair x = - x |> `(fn x => x + 1) - |> (fn (x, y) => (x, y + 1))*} - -text {* - takes @{text x} as argument, and then increments @{text x}, but also keeps - @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)" - for x}. After that, the function increments the right-hand component of the - pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}. - - The combinators @{ML "|>>"} and @{ML "||>"} are defined for - functions manipulating pairs. The first applies the function to - the first component of the pair, defined as -*} - -ML{*fun (x, y) |>> f = (f x, y)*} - -text {* - and the second combinator to the second component, defined as -*} - -ML{*fun (x, y) ||> f = (x, f y)*} - -text {* - With the combinator @{ML "|->"} you can re-combine the elements from a pair. - This combinator is defined as -*} - -ML{*fun (x, y) |-> f = f x y*} - -text {* and can be used to write the following roundabout version - of the @{text double} function: -*} - -ML{*fun double x = - x |> (fn x => (x, x)) - |-> (fn x => fn y => x + y)*} - -text {* - Recall that @{ML "|>"} is the reverse function applications. Recall also that the related - reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, - @{ML "|>>"} and @{ML "||>"} described above have related combinators for function - composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, - for example, the function @{text double} can also be written as: -*} - -ML{*val double = - (fn x => (x, x)) - #-> (fn x => fn y => x + y)*} - -text {* - - (FIXME: find a good exercise for combinators) -*} - +(* FIXME: some code below *) (*<*) setup {* diff -r 748d9c1a32fb -r fcc0e6e54dca CookBook/Intro.thy --- a/CookBook/Intro.thy Thu Feb 19 01:09:16 2009 +0000 +++ b/CookBook/Intro.thy Thu Feb 19 14:44:53 2009 +0000 @@ -15,7 +15,7 @@ against recent versions of Isabelle. If something does not work, then please let us know. If you have comments, criticism or like to add to the tutorial, feel free---you are most welcome! The tutorial is meant to be - gentle and comprehensive. To achieve this we need your feedback. + gentle and comprehensive. To achieve this we need your feedback. *} section {* Intended Audience and Prior Knowledge *} diff -r 748d9c1a32fb -r fcc0e6e54dca CookBook/Package/Ind_Interface.thy --- a/CookBook/Package/Ind_Interface.thy Thu Feb 19 01:09:16 2009 +0000 +++ b/CookBook/Package/Ind_Interface.thy Thu Feb 19 14:44:53 2009 +0000 @@ -245,15 +245,6 @@ predicates, the names and types of their parameters, the actual introduction rules and a \emph{local theory}. They return a local theory containing the definition and the induction principle as well introduction rules. - - In contrast to an ordinary theory, which simply consists of a type - signature, as well as tables for constants, axioms and theorems, a local - theory also contains additional context information, such as locally fixed - variables and local assumptions that may be used by the package. The type - @{ML_type local_theory} is identical to the type of \emph{proof contexts} - @{ML_type "Proof.context"}, although not every proof context constitutes a - valid local theory. - Note that @{ML add_inductive_i in SimpleInductivePackage} expects the types of the predicates and parameters to be specified using the diff -r 748d9c1a32fb -r fcc0e6e54dca CookBook/Parsing.thy --- a/CookBook/Parsing.thy Thu Feb 19 01:09:16 2009 +0000 +++ b/CookBook/Parsing.thy Thu Feb 19 14:44:53 2009 +0000 @@ -527,7 +527,7 @@ in which the @{text [quotes] "\\n"} causes the second token to be in line 8. - Now by using the parser @{ML OuterParse.position} you can decode the positional + By using the parser @{ML OuterParse.position} you can decode the positional information and return it as part of the parsed input. For example @{ML_response_fake [display,gray] @@ -563,7 +563,7 @@ The function @{ML OuterParse.prop} is similar, except that it gives a different error message, when parsing fails. Looking closer at the result string you will have noticed that the parser not just returns the parsed string, but also some - encoded positional information. You can see this better if you replace + encoded information. You can see this better if you replace @{ML Position.none} by @{ML "(Position.line 42)"}, say. @{ML_response [display,gray] @@ -574,7 +574,7 @@ end" "(\"\\^E\\^Ftoken\\^Fline=42\\^Fend_line=42\\^Efoo\\^E\\^F\\^E\", [])"} - The positional information is stored so that code called later will be + The positional information is stored so that code called later on will be able to give more precise error messages. *} @@ -606,18 +606,21 @@ *} ML %linenosgray{*val spec_parser = - OuterParse.opt_target -- - OuterParse.fixes -- - OuterParse.for_fixes -- - Scan.optional - (OuterParse.$$$ "where" |-- - OuterParse.!!! - (OuterParse.enum1 "|" - (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} + OuterParse.opt_target -- + OuterParse.fixes -- + OuterParse.for_fixes -- + Scan.optional + (OuterParse.$$$ "where" |-- + OuterParse.!!! + (OuterParse.enum1 "|" + (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} text {* - Note that the parser does not parse the ketword \simpleinductive. This - will be done by the infrastructure that will eventually call this parser. + Note that the parser does not parse the keyword \simpleinductive, even if it is + meant to process definitions as shown above. The parser of the keyword + will be given by the infrastructure that will eventually calls @{ML spec_parser}. + + To see what the parser returns, let us parse the string corresponding to the definition of @{term even} and @{term odd}: @@ -638,9 +641,10 @@ ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} As can be seen, the result is a ``nested'' four-tuple consisting of an - optional locale; a list of variables with optional type-annotation and - syntax-annotation; a list of for-fixes (fixed variables); and a list of rules - where each rule has optionally a name and an attribute. + optional locale (in this case @{ML NONE}); a list of variables with optional + type-annotation and syntax-annotation; a list of for-fixes (fixed variables; in this + case there are none); and a list of rules where every rule has optionally a name and + an attribute. In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target in order to indicate a locale in which the specification is made. For example @@ -648,8 +652,8 @@ @{ML_response [display,gray] "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"} - returns the locale @{text [quotes] "test"}; if no target is given' like in the - casde of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}. + returns the locale @{text [quotes] "test"}; if no target is given, like in the + case of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}. The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated list of variables that can include optional type annotations and syntax translations. @@ -671,7 +675,7 @@ text {* Whenever types are given, they are stored in the @{ML SOME}s. Since types - are part of the inner syntax they are strings with some printing directives + are part of the inner syntax they are strings with some encoded information (see previous section). If a syntax translation is present for a variable, then it is stored in the @{ML Mixfix} datastructure; no syntax translation is @@ -701,7 +705,6 @@ (name, map Args.dest_src attrib) end" "(foo_lemma, [((\"intro\", []), \), ((\"dest\", [\]), \)])"} - A name of a theorem can be quite complicated, as it can include attrinutes. The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some attributes. If you want to print out all currently known attributes a theorem @@ -714,7 +717,7 @@ \"} - For the inductive definitions described above only, the attibutes @{text "[intro]"} and + For the inductive definitions described above only the attibutes @{text "[intro]"} and @{text "[simp]"} make sense. \begin{readmore} diff -r 748d9c1a32fb -r fcc0e6e54dca CookBook/Tactical.thy --- a/CookBook/Tactical.thy Thu Feb 19 01:09:16 2009 +0000 +++ b/CookBook/Tactical.thy Thu Feb 19 14:44:53 2009 +0000 @@ -398,8 +398,6 @@ (*<*)oops(*>*) text {* - (FIXME: is it important to get the number of subgoals?) - The function @{ML resolve_tac} is similar to @{ML rtac}, except that it expects a list of theorems as arguments. From this list it will apply the first applicable theorem (later theorems that are also applicable can be diff -r 748d9c1a32fb -r fcc0e6e54dca cookbook.pdf Binary file cookbook.pdf has changed