--- a/ProgTutorial/Base.thy Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Base.thy Mon Aug 27 10:24:10 2012 +0100
@@ -1,9 +1,10 @@
theory Base
imports Main
"~~/src/HOL/Library/LaTeXsugar"
-keywords "ML" "setup" "local_setup" :: thy_decl and
+(*keywords "ML" "setup" "local_setup" :: thy_decl and
"ML_prf" :: prf_decl and
"ML_val" :: diag
+*)
uses
("output_tutorial.ML")
("antiquote_setup.ML")
--- a/ProgTutorial/Essential.thy Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Essential.thy Mon Aug 27 10:24:10 2012 +0100
@@ -1322,6 +1322,8 @@
ML {* Sign.classes_of @{theory} *}
+ML {* Sign.of_sort @{theory} *}
+
text {*
\begin{readmore}
Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
@@ -2014,6 +2016,7 @@
apply(auto)
done
+
text {*
While the information about which theorems are used is obvious in
the first two proofs, it is not obvious in the third, because of the
@@ -2023,7 +2026,7 @@
extracting this information. Let us first extract the name of the
established theorem. This can be done with
- @{ML_response [display,gray]
+ @{ML_response_fake [display,gray]
"@{thm my_conjIa}
|> Thm.proof_body_of
|> get_names"
@@ -2037,7 +2040,7 @@
and @{thm [source] conjunct2}. We can obtain them by descending into the
first level of the proof-tree, as follows.
- @{ML_response [display,gray]
+ @{ML_response_fake [display,gray]
"@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
@@ -2051,7 +2054,7 @@
proof in Isabelle. Note also that applications of @{text assumption} do not
count as a separate theorem, as you can see in the following code.
- @{ML_response [display,gray]
+ @{ML_response_fake [display,gray]
"@{thm my_conjIb}
|> Thm.proof_body_of
|> get_pbodies
@@ -2064,7 +2067,7 @@
and @{thm [source] my_conjIb}, as can be seen by the theorems that
are returned for @{thm [source] my_conjIc}.
- @{ML_response [display,gray]
+ @{ML_response_fake [display,gray]
"@{thm my_conjIc}
|> Thm.proof_body_of
|> get_pbodies
@@ -2079,7 +2082,7 @@
means we obtain the theorems that are used in order to prove
@{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
- @{ML_response [display, gray]
+ @{ML_response_fake [display, gray]
"@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
--- a/ProgTutorial/Intro.thy Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Intro.thy Mon Aug 27 10:24:10 2012 +0100
@@ -27,7 +27,8 @@
The best way to get to know the ML-level of Isabelle is by experimenting
with the many code examples included in the tutorial. The code is as far as
possible checked against the Isabelle
- distribution.\footnote{\input{version}} If something does not work, then
+ distribution. %FIXME \footnote{\input{version}}
+ If something does not work, then
please let us know. It is impossible for us to know every environment,
operating system or editor in which Isabelle is used. If you have comments,
criticism or like to add to the tutorial, please feel free---you are most
@@ -331,10 +332,10 @@
with TBD.}
\vfill
-
- This document (version \input{tip}\hspace{-0.5ex}) was compiled with:\\
- \input{version}\\
- %%\input{pversion}
+ %% FIXME
+ %% This document (version \input{tip.tex}\hspace{-0.5ex}) was compiled with:\\
+ %% \input{version}\\
+ %% \input{pversion}
*}
end
--- a/ProgTutorial/Package/Ind_Interface.thy Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy Mon Aug 27 10:24:10 2012 +0100
@@ -134,7 +134,7 @@
spec_parser >>
(fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
-val _ = Outer_Syntax.local_theory ("simple_inductive2", Keyword.thy_decl)
+val _ = Outer_Syntax.local_theory @{command_spec "simple_inductive2"}
"definition of simple inductive predicates"
specification*}
--- a/ProgTutorial/Package/simple_inductive_package.ML Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML Mon Aug 27 10:24:10 2012 +0100
@@ -236,7 +236,7 @@
(fn (((loc, preds), params), specs) =>
Toplevel.local_theory loc (add_inductive preds params specs))
-val _ = Outer_Syntax.command ("simple_inductive", Keyword.thy_decl) "define inductive predicates"
+val _ = Outer_Syntax.command @{command_spec "simple_inductive"} "define inductive predicates"
specification
(* @end *)
--- a/ProgTutorial/Recipes/Oracle.thy Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy Mon Aug 27 10:24:10 2012 +0100
@@ -57,7 +57,7 @@
the string, we use functions from the @{text Buffer} module.
*}
-ML {*fun translate t =
+ML %grayML{*fun translate t =
let
fun trans t =
(case t of
@@ -72,8 +72,7 @@
Buffer.add n #>
Buffer.add " "
| _ => error "inacceptable term")
- in Buffer.content (trans t Buffer.empty) end
-*}
+ in Buffer.content (trans t Buffer.empty) end*}
text {*
Here is the string representation of the term @{term "p = (q = p)"}:
--- a/ProgTutorial/document/root.tex Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/document/root.tex Mon Aug 27 10:24:10 2012 +0100
@@ -17,6 +17,7 @@
\usepackage{index}
\usepackage{tocbibind}
\usepackage{tikz}
+\usepackage{bashful}
\usetikzlibrary{shadows}
\usepackage{pdfsetup}
Binary file progtutorial.pdf has changed