adapted to new build framework
authorChristian Urban <urbanc@in.tum.de>
Mon, 27 Aug 2012 10:24:10 +0100
changeset 535 5734ab5dd86d
parent 534 0760fdf56942
child 536 31d06b5cada4
adapted to new build framework
ProgTutorial/Base.thy
ProgTutorial/Essential.thy
ProgTutorial/Intro.thy
ProgTutorial/Package/Ind_Interface.thy
ProgTutorial/Package/simple_inductive_package.ML
ProgTutorial/Recipes/Oracle.thy
ProgTutorial/document/root.tex
progtutorial.pdf
--- 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