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;

modernized header;

modernized header;

obsolete;

modernized header;

obsolete;

modernized header;

modernized header;

modernized header;

modernized header;

modernized header;

modernized header;

modernized header;

clarified legacy command;

modernized header;

obsolete;

added update_header tool;

modernized header;

more flexibile \setisabellecontext, independently of header;

prefer explicit heading command;

uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;

eliminated dead code;

clarified syntax -- avoid overlap with command category;

tuned signature (see ab2483fad861);

recover via scanner; tuned signature;

simplified -- scanning is never interactive;

tuned signature, in accordance to Scala version;

command-line terminator ";" is no longer accepted;

eliminated spurious semicolons;

eliminated former Proof General preferences;

merged

tuned;

provide explicit theory (amending 621c052789b4);

removed pointless markup; tuned comments;

discontinued obsolete \<^sync> marker;