2010-10-16 wenzelm 2010-10-16 more robust treatment of symbolic indentifiers (which may contain colons);
2010-10-16 wenzelm 2010-10-16 more examples;
2010-10-16 wenzelm 2010-10-16 tuned;
2010-10-16 wenzelm 2010-10-16 more on "Exceptions"; tuned;
2010-10-15 wenzelm 2010-10-15 more on "Exceptions";
2010-10-15 wenzelm 2010-10-15 more examples;
2010-10-15 wenzelm 2010-10-15 tuned chapter arrangement;
2010-10-15 wenzelm 2010-10-15 more examples; tuned;
2010-10-15 wenzelm 2010-10-15 moved bind_thm(s) to implementation manual;
2010-10-14 wenzelm 2010-10-14 more on "Attributes"; tuned;
2010-10-14 wenzelm 2010-10-14 misc tuning and clarification;
2010-10-13 wenzelm 2010-10-13 more on "Proof methods"; more examples; tuned;
2010-10-13 wenzelm 2010-10-13 examples in Isabelle/HOL; tuned;
2010-10-13 wenzelm 2010-10-13 more on Proof.theorem;
2010-10-13 wenzelm 2010-10-13 tuned;
2010-10-12 wenzelm 2010-10-12 more examples; more on "Proof methods";
2010-10-12 wenzelm 2010-10-12 more on "Isar language elements";
2010-10-11 wenzelm 2010-10-11 more examples;
2010-10-11 wenzelm 2010-10-11 more refs;
2010-10-11 wenzelm 2010-10-11 misc tuning;
2010-10-10 wenzelm 2010-10-10 removed some obsolete reference material;
2010-10-10 wenzelm 2010-10-10 cover some more theory operations;
2010-10-10 wenzelm 2010-10-10 note on Isabelle file specifications; removed junk;
2010-10-10 wenzelm 2010-10-10 modernized version of "Message output channels";
2010-10-10 wenzelm 2010-10-10 removed some really old reference material;
2010-10-09 wenzelm 2010-10-09 more examples;
2010-10-09 wenzelm 2010-10-09 various concrete ML antiquotations;
2010-10-09 wenzelm 2010-10-09 prefer checked antiquotations;
2010-10-09 wenzelm 2010-10-09 clarified tag markup;
2010-10-08 wenzelm 2010-10-08 more on ML antiquotations; tuned;
2010-10-08 wenzelm 2010-10-08 keep normal size for %mlref tag;
2010-10-08 wenzelm 2010-10-08 basic setup for ML antiquotations -- with rail diagrams; tuned;
2010-10-08 wenzelm 2010-10-08 eliminated "Toplevel control", which belongs to TTY/ProofGeneral model;
2010-10-08 wenzelm 2010-10-08 eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX); eliminated Isar toplevel invocation functions, which belong to TTY/ProofGeneral model; moved remaining "ML toplevel" material to "Compile-time context";
2010-10-08 wenzelm 2010-10-08 misc tuning;
2010-10-07 wenzelm 2010-10-07 more on Isabelle/ML;
2010-10-07 wenzelm 2010-10-07 basic setup for Chapter 0: Isabelle/ML;
2010-10-07 wenzelm 2010-10-07 minor tuning and updating;
2010-10-01 wenzelm 2010-10-01 made SML/NJ happy;
2010-10-01 wenzelm 2010-10-01 merged
2010-10-01 haftmann 2010-10-01 use module integer for Eval
2010-10-01 haftmann 2010-10-01 check whole target hierarchy for existing reserved symbols
2010-10-01 haftmann 2010-10-01 added polyml_as_definition -- using external SML files as substitute for proper definitions -- only for polyml!
2010-10-01 wenzelm 2010-10-01 tuned default "Prover Session" perspective;
2010-10-01 wenzelm 2010-10-01 eliminated ancient OldTerm.term_frees;
2010-10-01 wenzelm 2010-10-01 more antiquotations;
2010-10-01 wenzelm 2010-10-01 simplified outer syntax setup; slightly more uniform Isabelle/ML indentation style;
2010-10-01 haftmann 2010-10-01 chop_while replace drop_while and take_while
2010-10-01 haftmann 2010-10-01 merged
2010-09-30 haftmann 2010-09-30 take_while, drop_while
2010-09-30 huffman 2010-09-30 rename cont2cont_split to cont2cont_prod_case; add lemmas prod_contI, prod_cont_iff; simplify some proofs
2010-09-30 huffman 2010-09-30 fixrec: rename match_cpair to match_Pair
2010-09-15 huffman 2010-09-15 remove code for obsolete 'fixpat' command
2010-09-15 huffman 2010-09-15 clean up definition of compile_pat function
2010-09-15 huffman 2010-09-15 rename some fixrec pattern-match compilation functions
2010-09-30 bulwahn 2010-09-30 adding example for case expressions
2010-09-30 bulwahn 2010-09-30 applying case beta reduction to case term before matching in predicate compile function flattening; moving case beta reduction function to Predicate_Compile_Aux
2010-09-30 bulwahn 2010-09-30 merged
2010-09-30 bulwahn 2010-09-30 adapting manual configuration in examples
2010-09-30 bulwahn 2010-09-30 finding the counterexample with different options (manually limited precisely, manually limited global, automatically limited global)