# HG changeset patch # User Christian Urban # Date 1235830682 0 # Node ID c22b507e1407c17ff39b81d8f411dc84235d8a41 # Parent 8084c353d19647149482009bc05017bd9c7cca66 general polishing; added versioning to the document diff -r 8084c353d196 -r c22b507e1407 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Fri Feb 27 15:59:38 2009 +0000 +++ b/CookBook/FirstSteps.thy Sat Feb 28 14:18:02 2009 +0000 @@ -962,8 +962,8 @@ is meant to be more than just for testing purposes! Here it is only used to illustrate matters. We will show later how to store data properly without using references. The function @{ML Thm.declaration_attribute} expects us to - provide two functions that add and delete theorems from this list. At - the moment we use the two functions: + provide two functions that add and delete theorems from this list. + For this we use the two functions: *} ML{*fun my_thms_add thm ctxt = @@ -1114,10 +1114,10 @@ data. \end{readmore} - What are: + (FIXME What are: @{text "theory_attributes"} - @{text "proof_attributes"} + @{text "proof_attributes"}) \begin{readmore} @@ -1126,7 +1126,7 @@ *} -section {* Theories, Contexts and Local Theories *} +section {* Theories, Contexts and Local Theories (TBD) *} text {* (FIXME: expand) @@ -1148,7 +1148,7 @@ -section {* Storing Theorems\label{sec:storing} *} +section {* Storing Theorems\label{sec:storing} (TBD) *} text {* @{ML PureThy.add_thms_dynamic} *} @@ -1178,7 +1178,13 @@ thm foo_def (*>*) -section {* Misc *} +section {* Pretty-Printing (TBD) *} + +text {* + @{ML Pretty.big_list} +*} + +section {* Misc (TBD) *} ML {*DatatypePackage.get_datatype @{theory} "List.list"*} diff -r 8084c353d196 -r c22b507e1407 CookBook/Intro.thy --- a/CookBook/Intro.thy Fri Feb 27 15:59:38 2009 +0000 +++ b/CookBook/Intro.thy Sat Feb 28 14:18:02 2009 +0000 @@ -48,9 +48,9 @@ now, but some parts, particularly the chapters on tactics, are still useful. - \item[The Isar Reference Manual] is also an older document that provides - material about Isar and its implementation. Some material in it - is still useful. + \item[The Isar Reference Manual] provides specification material (like grammars, + examples and so on) about Isar and its implementation. It is currently in + the process of being updated. . \end{description} Then of course there is: @@ -136,7 +136,20 @@ \end{itemize} Please let me know of any omissions. Responsibility for any remaining - errors lies with me. + errors lies with me.\bigskip + + {\Large\bf + This document is still in the process of being written! All of the + text is still under constructions. Sections and + chapters that are under \underline{heavy} construction are marked + with TBD.} + + + \vfill + This document was compiled with:\\ + \input{version} *} + + end \ No newline at end of file diff -r 8084c353d196 -r c22b507e1407 CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Fri Feb 27 15:59:38 2009 +0000 +++ b/CookBook/Recipes/Antiquotes.thy Sat Feb 28 14:18:02 2009 +0000 @@ -16,6 +16,9 @@ various entities in a document. They can also be used for sophisticated \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you obtain a list of all currently available document antiquotations and their options. + You obtain the same list on the ML-level by typing + + @{ML [display,gray] "ThyOutput.print_antiquotations ()"} Below we give the code for two additional antiquotations that can be used to typeset ML-code and also to check whether the given code actually compiles. This diff -r 8084c353d196 -r c22b507e1407 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Fri Feb 27 15:59:38 2009 +0000 +++ b/CookBook/Tactical.thy Sat Feb 28 14:18:02 2009 +0000 @@ -1015,7 +1015,7 @@ *} -section {* Simplifier Tactics *} +section {* Simplifier Tactics (TBD) *} text {* A lot of convenience in the reasoning with Isabelle derives from its @@ -1063,7 +1063,8 @@ typical of the form \begin{isabelle} - \mbox{\inferrule{@{text "contr t\<^isub>1\t\<^isub>n \ contr s\<^isub>1\s\<^isub>n"}}{@{text "t\<^isub>i \ s\<^isub>i"}}} + \mbox{\inferrule{@{text "t\<^isub>i \ s\<^isub>i"}} + {@{text "contr t\<^isub>1\t\<^isub>n \ contr s\<^isub>1\s\<^isub>n"}}} \end{isabelle} with @{text "constr"} being a term-constructor. However there are also more complicated @@ -1089,6 +1090,58 @@ The most frequently used simpsets in HOL are @{ML HOL_basic_ss} and @{ML HOL_ss}. *} +ML {* warning (Pretty.string_of (MetaSimplifier.pretty_ss HOL_ss)) *} + +ML {* +fun get_parts ss = +let + val ({rules, ...}, {congs, procs, loop_tacs, solvers, ...}) = MetaSimplifier.rep_ss ss +in + (rules, congs, procs, loop_tacs, solvers) +end +*} + +ML {* + Pretty.big_list +*} + + +ML {* +fun print_ss ss = + let + val pretty_thms = map (enclose " " "\n" o Display.string_of_thm) + + fun pretty_cong (name, {thm, lhs}) = + name ^ ":" ^ (Display.string_of_thm thm); + + val (rules, congs, procs, loop_tacs, solvers) = get_parts ss; + val smps = map #thm (Net.entries rules); + + in + "simplification rules:\n" ^ + (implode (pretty_thms smps)) ^ + "congruences:" ^ (commas (map pretty_cong (fst congs))) ^ "\n" ^ + "loopers:" ^ (commas (map (quote o fst) loop_tacs)) + end; +*} + +thm FalseE + +thm simp_impliesI +lemma "P (Suc 0) \ P ?x" +apply(tactic {* CHANGED (simp_tac HOL_basic_ss 1) *}) +oops + +ML {* warning (print_ss HOL_ss) *} + +text {* + @{ML HOL_basic_ss} can deal essentially only with goals of the form: + @{thm TrueI}, @{thm refl[no_vars]} @{term "x \ x"} and @{thm FalseE}, + and resolve with assumptions. +*} + +ML {* setsubgoaler *} + text {* (FIXME: what do the simplifier tactics do when nothing can be rewritten) diff -r 8084c353d196 -r c22b507e1407 IsaMakefile --- a/IsaMakefile Fri Feb 27 15:59:38 2009 +0000 +++ b/IsaMakefile Sat Feb 28 14:18:02 2009 +0000 @@ -19,8 +19,6 @@ rail CookBook/generated/root cp CookBook/generated/root.rao CookBook/document -## CookBook - tutorial: CookBook/ROOT.ML \ CookBook/document/root.tex \ CookBook/document/root.bib \ @@ -28,8 +26,9 @@ CookBook/*.ML \ CookBook/Recipes/*.thy \ CookBook/Package/*.thy \ - CookBook/Package/*.ML + CookBook/Package/*.ML $(USEDIR) HOL CookBook + $(ISATOOL) version > CookBook/generated/version $(ISATOOL) document -o pdf CookBook/generated @cp CookBook/document.pdf cookbook.pdf diff -r 8084c353d196 -r c22b507e1407 cookbook.pdf Binary file cookbook.pdf has changed