2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-11-09 nipkow 2014-11-09 avoid erule and rotated in IMP
2014-11-09 haftmann 2014-11-09 reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility
2014-11-09 haftmann 2014-11-09 self-contained simp rules for dvd on numerals
2014-11-08 haftmann 2014-11-08 equivalence rules for structures without zero divisors
2014-11-08 wenzelm 2014-11-08 removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-11-08 wenzelm 2014-11-08 clarified name of Type.unified, to emphasize its connection to the "unify" family; tuned low-level operation;
2014-11-08 wenzelm 2014-11-08 proper Envir.norm_type for result of Type.raw_unifys;
2014-11-08 wenzelm 2014-11-08 avoid slow metis proof;
2014-11-08 wenzelm 2014-11-08 proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);
2014-11-08 wenzelm 2014-11-08 tuned;
2014-11-08 wenzelm 2014-11-08 updated some sledgehammer proofs -- much faster;
2014-11-08 wenzelm 2014-11-08 updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);
2014-11-08 wenzelm 2014-11-08 recovered type matching, which was broken in 8a765db7e0f8 (see also 8a765db7e0f8, 2db1d3d2ed54); NB: "match" operates on direct substitution without variable chasing, in contrast to "unify" (and Unify.matches!) which work on cascaded env;
2014-11-08 wenzelm 2014-11-08 more direct type equality;
2014-11-08 haftmann 2014-11-08 reverted commit accident from 994fe0ba8335
2014-11-08 haftmann 2014-11-08 less space-wasting serialization setup: highest cell of array has been unused so far
2014-11-07 wenzelm 2014-11-07 tuned outline;
2014-11-07 wenzelm 2014-11-07 tuned syntax -- separate tokens;
2014-11-07 wenzelm 2014-11-07 eliminated pointless check -- command definitions are subject to theory context;
2014-11-07 wenzelm 2014-11-07 merged
2014-11-07 wenzelm 2014-11-07 prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors; tuned message;
2014-11-07 wenzelm 2014-11-07 tuned markup;
2014-11-07 wenzelm 2014-11-07 tuned;
2014-11-07 wenzelm 2014-11-07 clarified keyword categories; tuned;
2014-11-07 wenzelm 2014-11-07 tuned signature;
2014-11-07 wenzelm 2014-11-07 tuned;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-07 wenzelm 2014-11-07 proper import for command 'permanent_interpretation';
2014-11-07 wenzelm 2014-11-07 proper import of Main: BNF_Least_Fixpoint does not "contain pretty much everything", especially it lacks the 'value' command, which is defined *after* theory List;
2014-11-07 wenzelm 2014-11-07 more accurate keywords;
2014-11-06 wenzelm 2014-11-06 tuned signature;
2014-11-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-06 wenzelm 2014-11-06 proper Keyword.keywords (cf. 82a71046dce8);
2014-11-06 wenzelm 2014-11-06 prefer explicit Keyword.keywords (cf. 82a71046dce8);
2014-11-06 wenzelm 2014-11-06 tuned signature;
2014-11-06 wenzelm 2014-11-06 prefer explicit Keyword.keywords;
2014-11-06 wenzelm 2014-11-06 simplified keyword kinds; more explicit bootstrap syntax;
2014-11-07 paulson 2014-11-07 Tidying up. Removing unnecessary conditions from some theorems.
2014-11-07 traytel 2014-11-07 more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
2014-11-07 desharna 2014-11-07 document '*_transfer' attribute
2014-11-07 desharna 2014-11-07 document 'size_neq'
2014-11-07 desharna 2014-11-07 generate 'size_neq' for datatypes
2014-11-06 desharna 2014-11-06 fix 'unfla' function
2014-11-05 haftmann 2014-11-05 proper oriented equivalence of dvd predicate and mod
2014-11-05 wenzelm 2014-11-05 merged
2014-11-05 wenzelm 2014-11-05 more symbols;
2014-11-05 wenzelm 2014-11-05 tuned signature;
2014-11-05 wenzelm 2014-11-05 more uniform header_keywords in ML/Scala; tuned signature;
2014-11-05 wenzelm 2014-11-05 tuned;
2014-11-05 wenzelm 2014-11-05 more frugal keywords;
2014-11-05 wenzelm 2014-11-05 eliminated pointless dynamic keywords (TTY legacy);
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 tuned;
2014-11-05 wenzelm 2014-11-05 clarified representation of type Keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.Keywords;
2014-11-05 wenzelm 2014-11-05 clarified minor/major lexicon (like ML version);
2014-11-05 nipkow 2014-11-05 reduced execution time