--- 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"*}
--- 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
--- 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
--- 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\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>s\<^isub>n"}}{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}}
+ \mbox{\inferrule{@{text "t\<^isub>i \<equiv> s\<^isub>i"}}
+ {@{text "contr t\<^isub>1\<dots>t\<^isub>n \<equiv> contr s\<^isub>1\<dots>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) \<Longrightarrow> 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 \<equiv> x"} and @{thm FalseE},
+ and resolve with assumptions.
+*}
+
+ML {* setsubgoaler *}
+
text {*
(FIXME: what do the simplifier tactics do when nothing can be rewritten)
--- 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
Binary file cookbook.pdf has changed