2009-07-13 Christian Urban added section about code maintenance and added an example for antiquotations
2009-06-24 Christian Urban adapted to changes in Isabelle
2009-06-23 Christian Urban updated to new Isabelle
2009-06-05 Christian Urban updated to lates Isabelle changes
2009-06-04 Christian Urban minor tuning
2009-05-30 Christian Urban slightly modified index generation
2009-05-30 Christian Urban corrected index references and minor polishing
2009-05-30 Christian Urban added some first index-information
2009-05-30 Christian Urban added infrastructure for index; antiquotations have now the options [index] and [indexc]
2009-05-29 Christian Urban some slight polishing
2009-05-28 Christian Urban added comments about ML_prf and ML_val
2009-05-23 Christian Urban added an example
2009-05-18 Christian Urban a few additions
2009-05-17 Christian Urban some polishing; added together with Jasmin more examples to the pretty printing section
2009-05-09 Christian Urban slight polishing
2009-05-09 Christian Urban added more to the pretty section and updated the acknowledgements
2009-05-09 Christian Urban added some text to the pretty-printing section
2009-05-08 Christian Urban a saner method for calling PolyML
2009-05-08 Christian Urban Jasmin and Christian added examples for the pretty-printing section
2009-05-05 Christian Urban fixed the problem with double definition of even and odd
2009-04-28 Christian Urban slight polishing
2009-04-26 Christian Urban added note about @{type_names ...}
2009-04-25 Christian Urban polished
2009-04-25 Christian Urban replaced explode by Symbol.explode
2009-04-15 Christian Urban replaced "warning" with "writeln"
2009-04-13 Christian Urban added something about TRY and TRYALL
2009-04-11 Christian Urban very slight polishing to the simple inductive chapter
2009-04-09 Christian Urban some polishing
2009-04-08 Christian Urban explained uses and use commands
2009-04-08 Christian Urban polished
2009-04-08 Christian Urban added a section about naming conventions
2009-04-08 griff minor changes
2009-04-08 griff ran spell-checker
2009-04-07 Christian Urban added material about OuterKeyword.keyword and OuterParse.reserved
2009-04-07 Christian Urban permutation example uses now recent infrastructure
2009-04-03 Christian Urban various additions
2009-04-02 Christian Urban merged
2009-04-01 griff * merge
2009-04-02 Christian Urban section for further material about simple inductive
2009-04-01 Christian Urban finished the heavy duty stuff for the inductive package
2009-04-01 Christian Urban merged
2009-04-01 Christian Urban merged
2009-03-30 griff corrected some typos
2009-03-30 griff polishing
2009-04-01 Christian Urban more work on the simple inductive chapter
2009-03-31 Christian Urban started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
2009-03-31 Christian Urban used antiquotations
2009-03-31 Christian Urban added a declaration section (for Amine)
2009-03-31 Christian Urban more work on the inductive package
2009-03-30 Christian Urban updated to latest Isabelle
2009-03-30 Christian Urban some polishing
2009-03-27 Christian Urban polishing
2009-03-27 Christian Urban more work on simple inductive and marked all sections that are still seriously incomplete with TBD
2009-03-26 Christian Urban more work on the simple inductive section
2009-03-25 Christian Urban soem slight polishing
2009-03-24 Christian Urban a bit more work on the simple-inductive package
2009-03-24 Christian Urban some polishing
2009-03-24 Christian Urban added a keyword file, but needs to re-generated whenever something changes with keywords in Isabelle
2009-03-24 Christian Urban added infrastructure to generate the keyword file for simple_inductive
2009-03-23 Christian Urban merged
2009-03-23 Christian Urban merged
2009-03-23 griff tiny changes
2009-03-23 griff passive of `build' = `built'
2009-03-23 griff small changes
2009-03-23 griff typos
2009-03-23 griff again spell-checker on FirstSteps
2009-03-23 griff used spell checker on `FirstSteps' + small changes
2009-03-23 griff fixed `str_of_thms' output in example + small changes
2009-03-23 griff corrected typos + some small reformulations
2009-03-23 Christian Urban some polishing
2009-03-23 Christian Urban polishing to the theorem attributes section
2009-03-21 Christian Urban some polishing
2009-03-19 Christian Urban polished some recipies
2009-03-19 Christian Urban more one the simple-inductive chapter
2009-03-19 Christian Urban made more of the transition from "CookBook" to "ProgTutorial"
2009-03-18 Christian Urban added lots of FIXMES
2009-03-18 Christian Urban added non-standard Latex-style
2009-03-18 Christian Urban made the Ackermann function example safer and included suggestions from MW
2009-03-18 Christian Urban some polishing
2009-03-18 Christian Urban some polishing
2009-03-17 Christian Urban a simplification suggested by Stefan and some polishing
2009-03-17 Christian Urban added hyperlinks for every file pointer
2009-03-17 Christian Urban updated to new method_setup
2009-03-17 Christian Urban added a recipy about SAT solvers
2009-03-16 Christian Urban more work on the simple-induct. chapter
2009-03-15 Christian Urban adapted to latest Attrib.setup changes and more work on the simple induct chapter
2009-03-13 Christian Urban polishing
2009-03-13 Christian Urban updated to new read_specification
2009-03-13 Christian Urban some polishing
2009-03-13 Christian Urban some minor polishing
2009-03-12 Christian Urban used latex package boxedminipage
2009-03-12 Christian Urban improved the solution for the simproc/conversion exercise
2009-03-12 Christian Urban simplified antiquotations
2009-03-12 boehmes merged
2009-02-26 boehmes Corrected small mistake.
2009-03-11 Christian Urban polished somewhat the recipes and solutions
2009-03-11 Christian Urban added temporarily some timing test about conversions and simprocs
2009-03-11 Christian Urban improvments to the solutions suggested by Sacha B?hme
2009-03-11 Christian Urban partially adapted to new antiquotation infrastructure
2009-03-10 Christian Urban more work on simple_inductive
2009-03-08 Christian Urban removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
2009-03-06 Christian Urban some additions to the simplifier section and general tuning
2009-03-06 Christian Urban rolled back the changes on the function warning and tracing
2009-03-05 Christian Urban redefined the functions warning and tracing in order to properly match more antiquotations
2009-03-04 Christian Urban updated to chages in binding module
2009-03-04 Christian Urban removed infix_conv and moved function no_vars into the FirstSteps chapter
2009-03-04 Christian Urban added more to the simplifier section
2009-03-03 Christian Urban polished
2009-03-02 Christian Urban tuned
2009-03-01 Christian Urban updated to repository version; added a section about timing
2009-02-28 Christian Urban general polishing; added versioning to the document
2009-02-27 Christian Urban added material to the endless story of the simplifier
2009-02-27 Christian Urban 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
2009-02-26 Christian Urban added a comment about Conv.fun_conv
2009-02-26 Christian Urban polished
2009-02-25 Christian Urban deleted Ad-hoc recipe
2009-02-25 Christian Urban more polishing of the conversion section
2009-02-25 Christian Urban some polishing about conversions
2009-02-25 Christian Urban some very slight polishing on the conversion section
2009-02-25 Christian Urban new pdf file
2009-02-25 Christian Urban merged with Sascha
2009-02-25 boehmes Polished conversion section.
2009-02-25 boehmes Merged with new cookbook.pdf.
2009-02-25 boehmes Removed cookbook.pdf.
2009-02-25 boehmes Improved conversion subsection.
2009-02-25 Christian Urban included comment from Sascha
2009-02-24 Christian Urban new pfd file
2009-02-24 Christian Urban to be in sync with Sascha
2009-02-24 boehmes First draft for conversions subsection.
2009-02-24 Christian Urban some slight polishing
2009-02-24 Christian Urban polishing and start of the section about attributes
2009-02-23 Christian Urban polished
2009-02-23 Christian Urban polished
2009-02-22 Christian Urban polished the section about simprocs and added an exercise
2009-02-22 Christian Urban started a section about simprocs
2009-02-21 Christian Urban polished
2009-02-20 Christian Urban updated and added two tentative recipes
2009-02-19 Christian Urban polished
2009-02-19 Christian Urban polished parser section
2009-02-18 Christian Urban added to the first-steps section
2009-02-17 Christian Urban some polishing in the first-steps chapter
2009-02-17 Christian Urban polished
2009-02-16 Christian Urban polishing
2009-02-15 Christian Urban some polishing; split up the file External Solver into two
2009-02-14 Christian Urban added an acknowledgement section
2009-02-14 Christian Urban polished and added more material to the package chapter
2009-02-14 Christian Urban added an option for linenumbers to the chunk-antiquotation
2009-02-14 Christian Urban more changes to the package chapter
2009-02-13 Christian Urban some update of the package introduction
2009-02-13 Christian Urban properly handled linenumbers in ML-text and Isar-proofs
2009-02-13 Christian Urban slightly updated
2009-02-13 Christian Urban improved
2009-02-12 Christian Urban rearranged some functions
2009-02-12 Christian Urban recovered old version of simple_induct; split the main function into small functions
2009-02-12 Christian Urban polished
2009-02-11 Christian Urban added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
2009-02-09 Christian Urban polished and more material in the tactic chapter
2009-02-09 Christian Urban renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious)
2009-02-09 Christian Urban added more to the Tactical section
2009-02-08 Christian Urban polished
2009-02-07 Christian Urban further cleanup
2009-02-07 Christian Urban general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
2009-02-06 Christian Urban tuned
2009-02-05 Christian Urban polished
2009-02-05 Christian Urban polished
2009-02-05 Christian Urban calculated the exact number of goals in the subgoal antiquotation
2009-02-05 Christian Urban changed the readmore environment
2009-02-05 Christian Urban (re)defined the document antiquotation @subgoal in order to be closer to what is actually printed
2009-02-04 Christian Urban added some preliminary notes about SUBPROOF
2009-01-30 boehmes rewrote recipes describing external solvers
2009-01-30 Christian Urban added
2009-01-29 Christian Urban tuned
2009-01-29 Christian Urban added a section that will eventually describe the code
2009-01-29 Christian Urban made chunks aware of the gray-option
2009-01-29 Christian Urban polishing
2009-01-29 Christian Urban adaptation of the package chapter to fit the rest
2009-01-28 Christian Urban updated version
2009-01-28 Christian Urban polished
2009-01-27 Christian Urban better handling of {* and *}
2009-01-27 Christian Urban some polishing
2009-01-27 Christian Urban fixed typos
2009-01-27 Christian Urban polished the combinator section
2009-01-26 Christian Urban polished
2009-01-26 Christian Urban tuned
2009-01-26 Christian Urban some tuning
2009-01-26 Christian Urban added a section about combinators
2009-01-26 Christian Urban changed definition of graybox
2009-01-24 Christian Urban adapted to changes in binding.ML
2009-01-23 Christian Urban tuned
2009-01-16 Christian Urban tuned
2009-01-15 Christian Urban used newly exported break reference in ThyOutput for writing separate output_list function
2009-01-14 Christian Urban added an antiquotation option [gray] for gray boxes around displays
2009-01-14 Christian Urban removed mytable from root-file
2009-01-14 Christian Urban deleted the fixme about simpsets
2009-01-14 Christian Urban highligted the background of ML-code
2009-01-14 Christian Urban added more to the "new command section" and tuning
2009-01-12 Christian Urban tuned
2009-01-12 Christian Urban tuned
2009-01-10 Christian Urban tuned and added a section about creating keyword files
2009-01-08 Christian Urban deleted old files and added code to give a special tag to the command ML
2009-01-08 Christian Urban tuned
2009-01-07 Christian Urban added Sacha as contributor
2009-01-07 boehmes Added four recipes.
2009-01-03 Christian Urban 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)
2008-12-17 Christian Urban tuned
2008-12-16 Christian Urban fixed typos
2008-12-16 berghofe Repaired output of marginal comments in ML antiquotation.
2008-12-16 Christian Urban added a para on Scan.unless and an exercise about scanning comments
2008-12-15 berghofe Adapted to changes in binding module.
2008-12-13 Christian Urban tuned; added document antiquotation ML_response_fake_both
2008-11-29 Christian Urban removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
2008-11-28 Christian Urban tuned
2008-11-28 Christian Urban completes the recipie on antiquotations
2008-11-25 Christian Urban tuned
2008-11-24 Christian Urban added more material
2008-11-01 Christian Urban fixed FIXME's in fake responses
2008-10-30 Christian Urban hakked latex so that it does not display ML {* *}; general tuning
2008-10-29 Christian Urban added a section about document antiquotations
2008-10-29 Christian Urban deleted old antiquote_setup and renamed antiquote_setup_plus to antiquuote_setup
2008-10-29 Christian Urban added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
2008-10-29 Christian Urban added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
2008-10-27 Christian Urban tuned mostly antiquotation and text
2008-10-20 Christian Urban further progress on the parsing section and tuning on the antiqu's
2008-10-17 Christian Urban more on the parsing section
2008-10-17 Christian Urban substantial changes to the antiquotations (preliminary version)
2008-10-14 Christian Urban added a preliminary section about parsing
2008-10-13 berghofe Adjusted margins.
2008-10-13 berghofe Updated.
2008-10-13 berghofe Tuned.
2008-10-13 berghofe Corrected typos.
2008-10-10 berghofe Updated.
2008-10-10 berghofe Added new chapter about writing packages.
2008-10-10 berghofe Added alltt, rail, and url.
2008-10-10 berghofe Added some more papers cited in the "how to write a package" chapter.
2008-10-10 berghofe Added rail style file.
2008-10-10 berghofe Added chapter about writing packages.
2008-10-10 berghofe Added chapter about writing packages.
2008-10-10 berghofe Added some more antiquotations.
2008-10-10 berghofe Antiquotation setup is now contained in theory Base.
2008-10-10 berghofe Antiquotation for referring to chunks of ML code.
2008-10-10 berghofe New theory for installing antiquotations.
2008-10-09 Christian Urban new version of implementation.aux
2008-10-09 Christian Urban added a proof and tuned the rest
2008-10-06 Christian Urban some slight polishing
2008-10-05 Christian Urban some tuning in the FirstSteps section
2008-10-02 Christian Urban tuned IsaMakefile
2008-10-02 Christian Urban fixed creation of bibliography
2008-10-02 Christian Urban polished
2008-10-02 Christian Urban added a solution section and some other minor additions
2008-10-02 Christian Urban added a paragraph about "uses" and started a paragraph about tracing
2008-10-02 Christian Urban polished and added a subdirectory for the recipes
2008-10-01 Christian Urban various changes by Alex and Christian
2008-09-30 Christian Urban tuned and updated antquote_setup.ML
2008-09-17 Christian Urban many changes in the FirstSteps section
2008-09-17 Christian Urban added new version
2008-09-15 Christian Urban forgot to add (see previous message)
2008-09-15 Christian Urban added an explicit file containing references in the Implementation manual (should be replaced by antiquotations)
2008-09-15 Christian Urban some tuning
2008-09-09 Christian Urban minor modifiations to the Intro and FirstSteps chapters
2008-09-06 Christian Urban added verbatim the notes by Jeremy
2008-09-05 Christian Urban not needed anymore -> moved to other places
2008-09-05 Christian Urban split the document into smaller pieces;
2008-09-03 Christian Urban added necessary files
2008-09-03 Christian Urban initial commit of Alexander's files
(0) tip