test

a few things added First_Steps

some tests

merged

minor things

updated to post-2011-1 Isabelle

a few things updated

this version works with Isabelle2011-1

updated to new Isabelle

updated to new Isabelle

binding in antiquotations

added an excercise originally by Jasmin Blanchette

more polishing

soem polishing

a little polishing

updated to new Isabelle

updated to new Isabelle

merged

updated to new Isabelle

updated

Updated to changes in timing structure

updated to new Isabelle

updated to post-2011 Isabelle

'Iff_Oracle.thy' has moved

'nat_number' was renamed to 'eval_nat_numeral'

tracing_fn was moved to Output.Private_Hooks

corrected AFP name

singular?

added missing 'of'

disabled foobar_prove; updated to new Isabelle

a bit closer to the new conventions of naming HOL-constants

updated to new isabelle

added something about Goal.prove_multi

tuned

added an example to be used for conversions later on

updated to new isabelle

merged

merged

updated to new isabelle

test

partially moved from string_of_term to pretty_term

updated for new isabelle

updated to new Isabelle

tuned

added something about raw_tactic

added Andreas

merged

tuning

some blabla about type classes, sorts, overloading, high level view on type classes

added some further ho-pat-unif examples but commented out (missing response check)

some more examples of ho-patterns

corrected def of ho-pat-unif, some extra hints about patterns

tuned

added example from Tobias and changed the title

updated to new Isabelle

added phi for morphisms

updated to new Isabelle

updated to new isabelle

updated to new Isabelle

added a section to the introduction; described @{make_string}

added something about ERROR and Fail

updated to new Isabelle

updated to new isabelle

typos fixed by Michael Norrish

updated to new Isabelle

a bit more tuning

polished

updated to new Isabelle

polised

polised the section about Subgoal.FOCUS

tuned

tuned

tunded

tuned

implemented suggestion from Sascha

improved section on conversions

added RANGE

added something about unifiacation and instantiations

tuned solution with comb_conv

updated to new Isabelle and clarified Skip_Proof

tuning

tuned

started something about sorts

tuned

tuned

spilt the Essential's chapter

updated to new Isabelle

tuned

modified the typ-pretty-printer and added parser exercise

added exercise

added example by Lukas Bulwahn

tuned

added Skip_Proof.mk_thm and some pointers about concurrency

completed the unification section

tuned

updated to new Isabelle

tuned

tuned

tuned

added more to the unification section

tuned

tuned

section about matching and unification of types

added a section about unification and matching

removed comment about compiler bug

added type work and updated to Isabelle and poly 5.3

tuned

added structure index

tuned

solved problem with mixfix.

added something about show_types references

tuned index

new parts in the tactical section

Proof.goal

tuned

avoid value restriction

modernized

tuned

added something about manual instantiations of theorems

tuned

tuned

polished

some polishing

included a comment from Tim Bourke

updated to new Isabelle

added something about add_thms_dynamic

some slight polishing

completed section on theorems

polished theorem section

updated to new Isabelle

polished

updated to Isabelle changes

tuned

slightly tuned

tuned the ML-output mechanism; tuned slightly the text

polished

added structures in the index

polished first chapter

fixed glitch with tocibind

more work on theorem section

more work

used a better implementation of \index in Latex; added more to the theorem section

more on the theorem section

a bit more work on the theorem section

polished on the pretty printing section

reorganised the certified terms section; tuned

tuned

added fixme

added the function unabs_def in the conversions section

used rewrite_goal_tac (instead of rewrite_goals_tac)

tuned

more work

updated to new Isabelle; more work on the data section

more work on the storing section

more work on the tutorial

started section about storing data

updated foobar_proof example

some polishing

included some tests

polished the commands section

tuned

added file for producing a keyword file

split up the first-steps section into two chapters

added an experimental antiquotation to replace eventually ML_response_fake

further polishing of index generation

simplified a bit the index generation

polished

polished the exercises about constructing terms

added exercise

polished

added some rudimentary inrastructure for producing the ML-code

tuned

improvements from the workshop

suggestions by Peter Homeier

tuned the section about printing several bits of inormation

added a comment for printing out information and tuned some examples accordingly

polished comment for error function

added an antiquotation for printing the raw proof state; polished the example about proof state

tuned

replaced "writeln" with "tracing"

removed rail; added external aux-files

updated to Isabelle changes and merged sections in the FirstSteps chapter

some general polishing

renamed pictures

tuned figure placement

polished the package chapter used FOCUS to explain the subproofs

made changes for SUBPROOF and sat_tac

slightly changed exercises about rev_sum

added more to the ML-antiquotation section

polished the section on conversions

slight change

adapted to changes in Isabelle

typo

typo

typo

spell checker

comment

typo

typo

typo

spell checked

reformulation

tuned

merged

label for exercise

show type of "x"

still merging

sync PDF

merged

modified solution(s) for "revsum" example

included an alternative solution for the "rev_sum" example as a comment

show the type of "x" in the formula

discussion of "const_name" before exercises

if n would be 0, rev_sum would be missing an argument

tuned

small changes for latest changes in Isabelle

minor tuning

added section about code maintenance and added an example for antiquotations

adapted to changes in Isabelle

updated to new Isabelle

updated to lates Isabelle changes

minor tuning

slightly modified index generation

corrected index references and minor polishing

added some first index-information

added infrastructure for index; antiquotations have now the options [index] and [indexc]

some slight polishing

added comments about ML_prf and ML_val

added an example

a few additions

some polishing; added together with Jasmin more examples to the pretty printing section

slight polishing

added more to the pretty section and updated the acknowledgements

added some text to the pretty-printing section

a saner method for calling PolyML

Jasmin and Christian added examples for the pretty-printing section

fixed the problem with double definition of even and odd

slight polishing

added note about @{type_names ...}

polished

replaced explode by Symbol.explode

replaced "warning" with "writeln"

added something about TRY and TRYALL

very slight polishing to the simple inductive chapter

some polishing

explained uses and use commands

polished

added a section about naming conventions

minor changes

ran spell-checker

added material about OuterKeyword.keyword and OuterParse.reserved

permutation example uses now recent infrastructure

various additions

merged

* merge

section for further material about simple inductive

finished the heavy duty stuff for the inductive package

merged

merged

corrected some typos

polishing

more work on the simple inductive chapter

started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)

used antiquotations

added a declaration section (for Amine)

more work on the inductive package

updated to latest Isabelle

some polishing

polishing

more work on simple inductive and marked all sections that are still seriously incomplete with TBD

more work on the simple inductive section

soem slight polishing

a bit more work on the simple-inductive package

some polishing

added a keyword file, but needs to re-generated whenever something changes with keywords in Isabelle

added infrastructure to generate the keyword file for simple_inductive

merged

merged

tiny changes

passive of `build' = `built'

small changes

typos

again spell-checker on FirstSteps

used spell checker on `FirstSteps' + small changes

fixed `str_of_thms' output in example + small changes

corrected typos + some small reformulations

some polishing

polishing to the theorem attributes section

some polishing

polished some recipies

more one the simple-inductive chapter

made more of the transition from "CookBook" to "ProgTutorial"

added lots of FIXMES

added non-standard Latex-style

made the Ackermann function example safer and included suggestions from MW

some polishing

some polishing

a simplification suggested by Stefan and some polishing

added hyperlinks for every file pointer

updated to new method_setup

added a recipy about SAT solvers

more work on the simple-induct. chapter

adapted to latest Attrib.setup changes and more work on the simple induct chapter

polishing

updated to new read_specification

some polishing

some minor polishing

used latex package boxedminipage

improved the solution for the simproc/conversion exercise

simplified antiquotations

merged

Corrected small mistake.

polished somewhat the recipes and solutions

added temporarily some timing test about conversions and simprocs

improvments to the solutions suggested by Sacha B?hme

partially adapted to new antiquotation infrastructure

more work on simple_inductive

removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive

some additions to the simplifier section and general tuning

rolled back the changes on the function warning and tracing

redefined the functions warning and tracing in order to properly match more antiquotations

updated to chages in binding module

removed infix_conv and moved function no_vars into the FirstSteps chapter

added more to the simplifier section

polished

tuned

updated to repository version; added a section about timing

general polishing; added versioning to the document

added material to the endless story of the simplifier

added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section

added a comment about Conv.fun_conv

polished

deleted Ad-hoc recipe

more polishing of the conversion section

some polishing about conversions

some very slight polishing on the conversion section

new pdf file

merged with Sascha

Polished conversion section.

Merged with new cookbook.pdf.

Removed cookbook.pdf.

Improved conversion subsection.

included comment from Sascha

new pfd file

to be in sync with Sascha

First draft for conversions subsection.

some slight polishing

polishing and start of the section about attributes

polished

polished

polished the section about simprocs and added an exercise

started a section about simprocs

polished

updated and added two tentative recipes

polished

polished parser section

added to the first-steps section

some polishing in the first-steps chapter

polished

polishing

some polishing; split up the file External Solver into two

added an acknowledgement section

polished and added more material to the package chapter

added an option for linenumbers to the chunk-antiquotation

more changes to the package chapter

some update of the package introduction

properly handled linenumbers in ML-text and Isar-proofs

slightly updated

improved

rearranged some functions

recovered old version of simple_induct; split the main function into small functions

polished

added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)

polished and more material in the tactic chapter

renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)

added more to the Tactical section

polished

further cleanup

general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution

tuned

polished

polished

calculated the exact number of goals in the subgoal antiquotation

changed the readmore environment

(re)defined the document antiquotation @subgoal in order to be closer to what is actually printed

added some preliminary notes about SUBPROOF

rewrote recipes describing external solvers

added

tuned

added a section that will eventually describe the code

made chunks aware of the gray-option

polishing

adaptation of the package chapter to fit the rest

updated version

polished

better handling of {* and *}

some polishing

fixed typos

polished the combinator section

polished

tuned

some tuning

added a section about combinators

changed definition of graybox

adapted to changes in binding.ML

tuned

tuned

used newly exported break reference in ThyOutput for writing separate output_list function

added an antiquotation option [gray] for gray boxes around displays

removed mytable from root-file

deleted the fixme about simpsets

highligted the background of ML-code

added more to the "new command section" and tuning

tuned

tuned

tuned and added a section about creating keyword files

deleted old files and added code to give a special tag to the command ML

tuned

added Sacha as contributor

Added four recipes.

doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)

tuned

fixed typos

Repaired output of marginal comments in ML antiquotation.

added a para on Scan.unless and an exercise about scanning comments

Adapted to changes in binding module.

tuned; added document antiquotation ML_response_fake_both

removed the @{ML ...} antiquotation in favour of @{ML_open ...x}

tuned

completes the recipie on antiquotations

tuned

added more material

fixed FIXME's in fake responses

hakked latex so that it does not display ML {* *}; general tuning

added a section about document antiquotations

deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup

added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual

added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit

tuned mostly antiquotation and text

further progress on the parsing section and tuning on the antiqu's

more on the parsing section

substantial changes to the antiquotations (preliminary version)

added a preliminary section about parsing

Adjusted margins.

Updated.

Tuned.

Corrected typos.

Updated.

Added new chapter about writing packages.

Added alltt, rail, and url.

Added some more papers cited in the "how to write a package" chapter.

Added rail style file.

Added chapter about writing packages.

Added chapter about writing packages.

Added some more antiquotations.

Antiquotation setup is now contained in theory Base.

Antiquotation for referring to chunks of ML code.

New theory for installing antiquotations.

new version of implementation.aux

added a proof and tuned the rest

some slight polishing

some tuning in the FirstSteps section

tuned IsaMakefile

fixed creation of bibliography

polished

added a solution section and some other minor additions

added a paragraph about "uses" and started a paragraph about tracing

polished and added a subdirectory for the recipes

various changes by Alex and Christian

tuned and updated antquote_setup.ML

many changes in the FirstSteps section

added new version

forgot to add (see previous message)

added an explicit file containing references in the Implementation manual (should be replaced by antiquotations)

some tuning

minor modifiations to the Intro and FirstSteps chapters

added verbatim the notes by Jeremy

not needed anymore -> moved to other places

split the document into smaller pieces; made it standalone by copying antiquote_setup.ML into the repository added cover page

added necessary files