merged

no quick_and_dirty for proof extraction, to avoid obscure errors like "corr: bad proof";

use \isastyletext directly via 'text' command;

proper sequential version (cf. 302104d8366b);

documentation stubs about permanent_interpretation

cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory

merged

import general theorems from AFP/Markov_Models

uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;

tuning

merged

do not introduce consts too early unnecessarily

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;

clarified minor/major lexicon (like ML version);

reduced execution time

proper button margins for Nimbus L&F; properties are sorted when saved;

approximative update of versions;

Added Option.bind_split{,_asm,s}

clarified legacy code;

eliminated unused int_only flag (see also c12484a27367); just proper commands;

eliminated obsolete Proof.goal_message -- print outcome more directly;

updated to scala-2.11.4;

less ambitious isatest: polyml-5.3.0 has problems with big sessions like HOL-Proofs;

modernized header uniformly as section;

prefer \setisabellecontext;