added lemma

merged

prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;

make SML/NJ happy;

more careful ML source positions, for improved PIDE markup;

NEWS

tuned proofs

added quickcheck[approximation]

quickcheck setup for float, inspired by rat::{exhaustive,full_exhaustive,random}

disjunction and conjunction for forms

truncate intermediate results in horner to improve performance of approximate; more efficient truncated addition float_plus_up/float_plus_down

added lemmas: convert between powr and log in comparisons, pull log out of addition/subtraction

cancel real of power of numeral also for equality and strict inequality; simplify floor of power of numeral; lemmas about real/floor

simplified computations based on round_up by reducing to round_down; more general round_up_le1, round_up_less1, round_down_ge1, round_up_le0

code equation for powr

merged

more careful ML source positions, for improved PIDE markup;

more position information, e.g. relevant for errors in generated ML source;

more symbols;

tuned whitespace;

more markup;

simplifie sessions;

more Isar proof methods;

more Isar proof methods;

more Isar proof methods;

add forgotten lemma

added lemma

make 'corec_transfer' tactic more robust

also generate '(co)rec_transfer' for (co)datatypes with 0 live type variables

make 'rec_transfer' tactic more robust

add del option to measurable; make measurability rules available as dynamic theorem;

merged

proper context for assume_tac (atac remains as fall-back without context);

even -> evn because even is now in Main

dropped redundant transfer rules (now proved and registered by datatype and plugins)

proper context for typedef;

proper proof context for typedef;

proper context;

proper context for match_tac etc.;

proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);

avoid erule and rotated in IMP

reverted 1ebf0a1f12a4 after successful re-tuning of simp rules for divisibility

self-contained simp rules for dvd on numerals

equivalence rules for structures without zero divisors

removed obsolete global-only options, which did not work out anyway (due to complexity of local_theory sandwich);

optional proof context for unify operations, for the sake of proper local options;

clarified name of Type.unified, to emphasize its connection to the "unify" family; tuned low-level operation;

proper Envir.norm_type for result of Type.raw_unifys;

avoid slow metis proof;

proper Envir.norm_type for result of Unify.unifiers (amending 479832ff2d29 from 20 years ago);

tuned;

updated some sledgehammer proofs -- much faster;

updated sledgehammer proof after breakdown of metis (exception Type.TUNIFY);

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;

more direct type equality;

reverted commit accident from 994fe0ba8335

less space-wasting serialization setup: highest cell of array has been unused so far

tuned outline;

tuned syntax -- separate tokens;

eliminated pointless check -- command definitions are subject to theory context;

merged

prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors; tuned message;

tuned markup;

tuned;

clarified keyword categories; tuned;

tuned signature;

tuned;

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;

proper import for command 'permanent_interpretation';

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;

more accurate keywords;

tuned signature;

more explicit Keyword.keywords;

proper Keyword.keywords (cf. 82a71046dce8);

prefer explicit Keyword.keywords (cf. 82a71046dce8);

tuned signature;

prefer explicit Keyword.keywords;

simplified keyword kinds; more explicit bootstrap syntax;

Tidying up. Removing unnecessary conditions from some theorems.

more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories

document '*_transfer' attribute

document 'size_neq'

generate 'size_neq' for datatypes

fix 'unfla' function

proper oriented equivalence of dvd predicate and mod

merged

more symbols;

tuned signature;

more uniform header_keywords in ML/Scala; tuned signature;

tuned;

more frugal keywords;

eliminated pointless dynamic keywords (TTY legacy);

explicit type Keyword.keywords; tuned signature;

tuned;

clarified representation of type Keywords; tuned signature;

explicit type Keyword.Keywords;