tuned whitespace

move instantiation here from AFP/Native_Word

dropped junk

postpone dis"useful" lemmas

cleanup

prefix disambiguation

tuned proofs and declarations

prefer target-style syntaxx for sublocale

prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm

self-contained formulation of subclass command, avoiding hard-wired Named_Target.init

ephemeral interpretation also formally works on theory level

abolished slightly odd global lattice interpretation for min/max

prefer more canonical names for lemmas on min/max

explicit distributivity facts on min/max

postponed min/max lemmas until abstract lattice is available

tuned structure of min/max lemmas

prefer abstract simp rule

more lemmas on abstract lattices

tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs

more general induction rule; tuned proofs

convenient printing of polynomial values

prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.

prefer Y_of_X over X_to_Y; prefer alist over assoc_list; prefer explicit prefix

merge

prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)

NEWS

dropped redundant lemma

syntactically tuned

prefer plain bool over dedicated type for binary digits

tuned

compile + reduce problem size by a notch

generate exhaust from nchotomy

made tactic work with theorems with multiple assumptions

renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)

express weak pullback property of bnfs only in terms of the relator

merged

tuned

reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)

tuning whitespace

recognize datatype reasoning in SPASS-Pirate

note manually proved exclusiveness property

note exhaust proof obligation

compile

implemented 'exhaustive' option in tactic

tuning

tuning

tuning 'case' expressions

don't do 'isar_try0' if preplaying is off

more data structure refactoring

data structure rationalization

tuning

refactored preplaying outcome data structure

distinguish not preplayed & timed out

pick up tfree/tvar type from SPASS-Pirate proof

tuning

extended ATP types with sorts

removed debugging output

honor SPASS-Pirate type arguments

made SML/NJ-friendlier (hopefully)

made timeouts in Sledgehammer not be 'option's -- simplified lots of code

simplified data structure

prevent curl's output to interfere with the prover's output

tuning

merge

parse SPASS-Pirate types

merged

added lemma

merge

pass down user input in more cases in order to preserve "let"s etc.

pass auto-proved exhaustiveness properties to tactic; rightly use "%_. False" instead of undefined for unspecified conditions; get rid of ugly "if True then ... else Code.abort" in auto-generated code equations;

merge

changed pirate port

fixed variable confusion introduced by 'tuning' change 565f9af86d67

made SML/NJ happier

try 'auto' first -- more likely to succeed

new port

tuning

generate type classes for tfrees

modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property

avoid clashes of fact names

initalize locale with idents from background theory rather than empty idents: must treat idents and registrations synchronously to provide consistent setup for interpretation in locale contexts

reduced cardinals dependencies of (co)datatypes

tighter bnf bounds for (co)datatypes

tuned

tuning

removed workaround

tuning

primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)

NEWS

merged

lemmas about divideR and scaleR

monotonicity of rounding and truncating float

Float: prevent unnecessary large numbers when adding 0

additional definitions and lemmas for Float

additional lemmas

summarized notions related to ordered_euclidean_space and intervals in separate theory

pragmatic executability of instance prod::{open,dist,norm}

introduced ordered real vector spaces

remove redundant constants

ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order

prefer box over greaterThanLessThan on euclidean_space

made SML/NJ happier

fixed source of 'Subscript' exception

handle Skolems gracefully for SPASS as well

move some Z3 specifics out (and into private repository with the rest of the Z3-specific code)

reverse Skolem function arguments

correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference

fixed confusion between 'prop' and 'bool' introduced in 4960647932ec

generalize method list further to list of list (clustering preferred methods together)

store alternative proof methods in Isar data structure

tuning

added 'meson' to the mix

tuning

made SML/NJ happy

use consistent condition for setting 'metis_new_skolem' (in preplaying and in output printing) + tuning

generate proper succedent for cases with trivial branches

tuning

simplify generated propositions

use 'prop' rather than 'bool' systematically in Isar reconstruction code

tuning

use 'arith' when appropriate in Z3 proofs

robustness in degenerate case + tuning

use simplifier for rewrite

more aggressive merging

implemented Z3 skolemization

inline Z3 hypotheses

merge

merge

merged

better handling of Z3 proof blocks

disambiguation of interpretation prefixes

more algebraic terminology for theories about big operators

more antiquotations;

proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;

merged

maintain morphism names for diagnostic purposes;

tuned -- prefer canonical argument order of fold_rev;

proper simplifier context; more standard "cert";

tuned;

tuned whitespace;

made SML/NJ happy + whitespace tuning

clarified Proof General legacy: special treatment of \<^newline> only in TTY mode;

merged

discontinued legacy_isub_isup;

clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;

skeleton for Simplifier trace by Lars Hupel;

generic trace operations for main steps of Simplifier;

tuned signature;

tuned whitespace;

added missing file (cf. 124432e77ecf);

tuned whitespace;

removed dead code -- ctxt is never visible (see also 658fcba35ed7);

simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;

tuned message;

be more explicit about pre- and postprocessor, particularly code_abbrev

removed obsolete codegen setup; Stream -> SCons; tuned

merged

tuned patterns;

support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;

reverse order in which lines are selected, to ensure that the number of dependencies is accurate

truncate proof once False is hit to avoid confusing the rest of the code (no idea why Z3 goes on)

removed inlined rewriting'' for one-branch case splits in Isar proofs, since these can yield huge unreadable formulas

Fib: Who needs the int version?

more work on Z3 Isar proofs

streamlined two proofs

merged

alternative hires icon;

NEWS

default code equations for make, fields, extend and truncate operations on records

browse directory hyperlink as well;

provide @{file_unchecked} in Isabelle/Pure;

tuned;

more antiquotations;

added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;

tuning -- moved ML files to subdirectory

adapted code for Z3 proof reconstruction

useful debugging info

disable generalization in MaSh until it is shown to help

bugfixes to Python MaSh related to alternative features

compile

generate problems with type classes

added warning to documentation, based on isabelle-users thread

more reasonable default weight

added multiple feature capability to MaSh

code equations for "local" (co)datatypes available after interpretation of locales with assumptions

more direct Isabelle_System.pdf_viewer; generic Isabelle_System.open, e.g. for URLs;

proper latex;

NEWS;

no keyboard control -- avoid confusion about meaning of selection;

directly react on click, assuming that document view operation is mostly idempotent;

generic $ISABELLE_OPEN;

updated to Sumatra PDF 2.4; prefer option -reuse-instance; PDF_VIEWER refers to program, not command-line;

clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;

tuned;

tuned proofs;

reverted 86e0b402994c, which was accidentally qfinish'ed and pushed

Better simprules and markup. Restored the natural number version of the binomial theorem

more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash; tuned signature;

strict EXEC_PROCESS: component can be expected to be present;

uniform use of transparent icons, as for main "apps";

more isabelle logos (from isabelle_transparent.ico);

recover 175b43e0b9ce from lost update in cc126144f662;

merged

relocate NEWS to post-release version (cf. 7a14f831d02d);

merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;

removed obsolete RC tags;

merged;

Added tag Isabelle2013-2 for changeset 4dd08fe126ba

remove junk;

recover main entry point from d9c88171b393 -- occasionally useful with plain "java -jar jedit.jar";

tuned;

tuned;

Added tag Isabelle2013-2-RC3 for changeset aeb21314d078

prefer transparent application icon (like Mac OS X);

specific application name for official bundle (as for Mac OS X);

prefer isabelle application icon;

more isabelle logos (from isabelle.ico);

prefer 32x32 icon like jedit (image from isabelle.ico);

updated isabelle.ico for the record (see also 84177f8372f9);

updated icon of Isabelle.exe, using http://convertico.org/image_to_icon_converter on lib/logo/isabelle.gif (approx. 256x256 pixels according to Windows 7 format);

further encouragement to read jEdit documentation;

clarified view.title;

NEWS;

non-focusable button, to avoid second interpretation of SPACE in C+e SPACE (isabelle.set-node-required);

more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;

Added tag Isabelle2013-2-RC2 for changeset 99b9249b3e05

more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec); tuned signature;

NEWS;

more defensive order of Markup.failed vs. Markup.finished -- more informative status in Isabelle/Scala, although it is not rendered in Isabelle/jEdit;

more robust status reports: avoid loosing information about physical events (see also 28d207ba9340, 2bc5924b117f, 9edfd36a0355) -- NB: TTY and Proof General ignore Output.status and Output.report; more defensive order of Markup.failed vs. Markup.finished, to allow breakdown of ML execution context (see also d7a1973b063c);

more robust and portable invocation of kill as bash builtin, instead of external executable -- NB: /bin/kill on Mac OS X Mountain Lion chokes on Linux workaround from 3610ae73cfdb;

Added tag Isabelle2013-2-RC1 for changeset 57aefb80b639

more on GTK;

reintroduced e2d08b9c9047, lost in 54e290da6da8 + e13b0c88c798 (clone of f6ffe53387ef);

NEWS;

back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command; resolve sendback wrt. static command id, to allow active area even after exec_id is removed (cf. prune_delay);

updated to Isabelle2013-2;

compile on Windows (clone of d04576557400);

register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37); tuned signature;

updated mirror script for Cambridge