# HG changeset patch # User Christian Urban # Date 1346059450 -3600 # Node ID 5734ab5dd86d8a4f5aa49b769610258b3becd31b # Parent 0760fdf56942a59a5fdf4d95c50d296399b11b45 adapted to new build framework diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Base.thy --- 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") diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Essential.thy --- 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 diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Intro.thy --- 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 diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Package/Ind_Interface.thy --- 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*} diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Package/simple_inductive_package.ML --- 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 *) diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Recipes/Oracle.thy --- 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)"}: diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/document/root.tex --- 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} diff -r 0760fdf56942 -r 5734ab5dd86d progtutorial.pdf Binary file progtutorial.pdf has changed