2012-02-18 haftmann tuned proofs
2012-02-12 haftmann tuned
2012-02-10 haftmann brute-force adjustion
2012-02-10 haftmann tuned whitespace
2012-02-10 haftmann tuned
2012-02-10 haftmann tuned
2012-02-10 haftmann tuned code
2012-02-10 haftmann dropped whitespace
2012-02-10 haftmann dropped dead code
2012-02-10 haftmann dropped dead code
2012-02-10 haftmann dropped dead code
2012-02-10 haftmann dropped dead code
2012-02-10 haftmann dropped dead code
2012-02-10 haftmann dropped dead code
2012-02-10 haftmann corrected typo
2012-02-10 haftmann dropped dead code
2012-02-12 haftmann notepad is more appropriate here
2012-02-18 boehmes corrected treatment of applications of built-in functions to higher-order terms
2012-02-18 krauss NEWS
2012-02-18 krauss merged
2012-02-18 krauss added congruence rules for Option.{map|bind}
2012-02-18 haftmann updated generated documents
2012-02-18 haftmann avoid redefinition of @{theory} antiquotation
2012-02-18 haftmann update of generated documents
2012-02-18 haftmann tuned whitespace
2012-02-18 haftmann clarified
2012-02-18 haftmann corrected spelling
2012-02-18 haftmann clarified
2012-02-18 haftmann more precise semantics of "theory" antiquotation
2012-02-18 haftmann tuned import
2012-02-18 haftmann dropped references to obsolete theories
2012-02-18 haftmann adjusted to set type constructor
2012-02-18 haftmann tuned whitespace
2012-02-18 haftmann more explicit error on malformed abstract equation; dropped dead code; tuned signature
2012-02-17 wenzelm simplified configuration options for syntax ambiguity;
2012-02-17 wenzelm retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
2012-02-16 wenzelm more antiquotations;
2012-02-16 wenzelm more symbols;
2012-02-16 wenzelm tuned imports;
2012-02-16 wenzelm tuned proofs;
2012-02-16 wenzelm simplified configuration options for syntax ambiguity;
2012-02-16 wenzelm merged
2012-02-16 bulwahn removing unnecessary premise from diff_single_insert
2012-02-16 wenzelm explicit is better than implicit;
2012-02-16 wenzelm more uniform / portable representation of the idea of "copy_dir" (NB: cp -f dereferences symlinks on GNU/Linux, but does not on old-school Unixen including BSD/Mac OS X);
2012-02-16 bulwahn simplifying proof
2012-02-16 bulwahn removing unnecessary premises in theorems of List theory
2012-02-16 bulwahn tuning mutabelle script
2012-02-16 bulwahn adding documentation for abort_potential option in quickcheck
2012-02-15 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2012-02-15 wenzelm discontinued Drule.term_rule, which tends to cause confusion due to builtin cterm_of (NB: the standard morphisms already provide a separate term component);
2012-02-15 wenzelm uniform Isar source formatting for this file;
2012-02-15 wenzelm clarified outer syntax "constdecl", which is only local to some rail diagrams;
2012-02-15 wenzelm discontinued obsolete "prems" fact;
2012-02-15 wenzelm eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
2012-02-15 wenzelm removed obsolete files;
2012-02-15 wenzelm more basic simplification, eliminated slightly odd tactic style from 1995 (cf. ea0668a1c0ba);
2012-02-15 wenzelm removed dead code;
2012-02-15 wenzelm updated listrel (cf. 80dccedd6c14);
2012-02-15 wenzelm removed redundant cut_inst_tac -- already covered in implementation manual;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip