2012-02-18 |
haftmann |
tuned proofs
|
changeset |
files
|
2012-02-12 |
haftmann |
tuned
|
changeset |
files
|
2012-02-10 |
haftmann |
brute-force adjustion
|
changeset |
files
|
2012-02-10 |
haftmann |
tuned whitespace
|
changeset |
files
|
2012-02-10 |
haftmann |
tuned
|
changeset |
files
|
2012-02-10 |
haftmann |
tuned
|
changeset |
files
|
2012-02-10 |
haftmann |
tuned code
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped whitespace
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped dead code
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped dead code
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped dead code
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped dead code
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped dead code
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped dead code
|
changeset |
files
|
2012-02-10 |
haftmann |
corrected typo
|
changeset |
files
|
2012-02-10 |
haftmann |
dropped dead code
|
changeset |
files
|
2012-02-12 |
haftmann |
notepad is more appropriate here
|
changeset |
files
|
2012-02-18 |
boehmes |
corrected treatment of applications of built-in functions to higher-order terms
|
changeset |
files
|
2012-02-18 |
krauss |
NEWS
|
changeset |
files
|
2012-02-18 |
krauss |
merged
|
changeset |
files
|
2012-02-18 |
krauss |
added congruence rules for Option.{map|bind}
|
changeset |
files
|
2012-02-18 |
haftmann |
updated generated documents
|
changeset |
files
|
2012-02-18 |
haftmann |
avoid redefinition of @{theory} antiquotation
|
changeset |
files
|
2012-02-18 |
haftmann |
update of generated documents
|
changeset |
files
|
2012-02-18 |
haftmann |
tuned whitespace
|
changeset |
files
|
2012-02-18 |
haftmann |
clarified
|
changeset |
files
|
2012-02-18 |
haftmann |
corrected spelling
|
changeset |
files
|
2012-02-18 |
haftmann |
clarified
|
changeset |
files
|
2012-02-18 |
haftmann |
more precise semantics of "theory" antiquotation
|
changeset |
files
|
2012-02-18 |
haftmann |
tuned import
|
changeset |
files
|
2012-02-18 |
haftmann |
dropped references to obsolete theories
|
changeset |
files
|
2012-02-18 |
haftmann |
adjusted to set type constructor
|
changeset |
files
|
2012-02-18 |
haftmann |
tuned whitespace
|
changeset |
files
|
2012-02-18 |
haftmann |
more explicit error on malformed abstract equation; dropped dead code; tuned signature
|
changeset |
files
|
2012-02-17 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
changeset |
files
|
2012-02-17 |
wenzelm |
retain default of Syntax.ambiguity, according to 2bd54d4b5f3d (despite earlier versions);
|
changeset |
files
|
2012-02-16 |
wenzelm |
more antiquotations;
|
changeset |
files
|
2012-02-16 |
wenzelm |
more symbols;
|
changeset |
files
|
2012-02-16 |
wenzelm |
tuned imports;
|
changeset |
files
|
2012-02-16 |
wenzelm |
tuned proofs;
|
changeset |
files
|
2012-02-16 |
wenzelm |
simplified configuration options for syntax ambiguity;
|
changeset |
files
|
2012-02-16 |
wenzelm |
merged
|
changeset |
files
|
2012-02-16 |
bulwahn |
removing unnecessary premise from diff_single_insert
|
changeset |
files
|
2012-02-16 |
wenzelm |
explicit is better than implicit;
|
changeset |
files
|
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);
|
changeset |
files
|
2012-02-16 |
bulwahn |
simplifying proof
|
changeset |
files
|
2012-02-16 |
bulwahn |
removing unnecessary premises in theorems of List theory
|
changeset |
files
|
2012-02-16 |
bulwahn |
tuning mutabelle script
|
changeset |
files
|
2012-02-16 |
bulwahn |
adding documentation for abort_potential option in quickcheck
|
changeset |
files
|
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;
|
changeset |
files
|
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);
|
changeset |
files
|
2012-02-15 |
wenzelm |
uniform Isar source formatting for this file;
|
changeset |
files
|
2012-02-15 |
wenzelm |
clarified outer syntax "constdecl", which is only local to some rail diagrams;
|
changeset |
files
|
2012-02-15 |
wenzelm |
discontinued obsolete "prems" fact;
|
changeset |
files
|
2012-02-15 |
wenzelm |
eliminated slightly odd / obsolete DETERM_UNTIL, DETERM_UNTIL_SOLVED (cf. 941afb897532, ea0668a1c0ba);
|
changeset |
files
|
2012-02-15 |
wenzelm |
removed obsolete files;
|
changeset |
files
|
2012-02-15 |
wenzelm |
more basic simplification, eliminated slightly odd tactic style from 1995 (cf. ea0668a1c0ba);
|
changeset |
files
|
2012-02-15 |
wenzelm |
removed dead code;
|
changeset |
files
|
2012-02-15 |
wenzelm |
updated listrel (cf. 80dccedd6c14);
|
changeset |
files
|
2012-02-15 |
wenzelm |
removed redundant cut_inst_tac -- already covered in implementation manual;
|
changeset |
files
|