maintain Version.syntax within document state; clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;

explicit Outer_Syntax.Decl;

allow multiple 'keywords' as in 'fixes'; tuned comments;

some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;

merged

merged

structured case and induct rules

rudimentary documentation test

doc-src build option (for emerging mira configuration)

corrected fragile proof; tuned semicolons

rudimentary distribution build configuration

support for non-HTTP repository locations (important for mira); quasi-hardwired repository name

corrected slip

merged

rationalising the induction rule trans_induct3

allow modification of REPOS_NAME and REPOS from outside

locale expressions without source positions;

tuned;

tuned messages;

source positions for locale and class expressions;

some proof indentation;

more explicit indication of swing thread context;

more indentation;

prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks; more robust use of Session.Commands_Changed vs. Document_View.visible_range as asynchronous swing task, taking into account that the model might have switched in the meantime (e.g. via fast clicking on hypersearch while the prover is crunching);

eliminated obsolete sanitize_name;

Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;

more parallel inductive_cases; more explicit indication of def names;

misc tuning;

updated to jedit_build-20120313 with jedit-4.5.0; updated version information;

tuned context specifications and proofs;

tuned proofs;

clarified command state -- markup within proper_range, excluding trailing whitespace;

more explicit indication of def names;

merged

Structured proofs concerning the square of an infinite cardinal

suppress vacous notes elements, with subtle change of semantics: 'interpret' no longer pulls-in unnamed facts "by fact";

prefer abs_def over def_raw;

prefer abs_def over def_raw;

improved attribute "abs_def" to handle object-equality as well;

merged

More structured proofs about cardinal arithmetic

tuned proofs;

refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;

tuned proofs -- eliminated pointless chaining of facts after 'interpret';

proper printing of empty binding (again, cf. 93f6f24010c2);

tuned;

tuned strip_alls;

allow redefining pretty/markup modes (not output due to bootstrap issues) -- to support reloading of theory src/HOL/src/Tools/Code_Generator;

some grouping of Par_List operations, to adjust granularity;

Par_List.map is already smart;

some support for grouped list operations;

merged;

merged

NEWS

use eventually_elim method

add eventually_elim method

merged

tuned proofs

tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set

tuned simpset

activate_notes in parallel -- to speedup main operation of locale interpretation;

refined activate_notes: simultaneous transformation before activation; actually export all_registrations_of;

tuned headers;

merged

Structured proofs in ZF

refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);

updated polyml/build option to prefer included libffi;

tuned signature;

clarified prepare_positions: always retain source positions to allow using it as formal information, not just markup reports;

merged

renewing Executable_Relation

tuned;

more direct Name_Space.defined_entry; tuned Variable.export_inst: avoid keeping full contexts within the gen_fixesT closure (NB: locale infrastructure stores morphisms persistently);

eliminated old-fashioned 'constrains' element;

modernized locale expression, with some fluctuation of arguments;

simplified span class in conformance to Scala version;

discontinued specific entity markup, which causes confusion with "kind" names with spaces (e.g. "type name"); uniform treatment of "class" entities in input and output;

merged

adding tags to quickcheck's result

clarified idents for activated locales, with subtle change of semantics: insert/merge wrt. term equality, but avoid redundant_ident on retrieval; avoid confusing quasiorder ident_le as "eq" for member/merge;

eliminated dead code;

clarified total_ident_ord, swapping first argument back to normal (unlike e464f84f3680) -- NB: "fast" ord is erratic anyway;

misc tuning and simplification;

tuned;

clarified Pattern.matchess;

tuned;

more precise alignment of begin/end, proof/qed; improved English;

merged

beautified

more precise checking for wellformedness of mapper, before and after morphism application

reject mapper terms with type variables not contained in the term's type

always bracket case expressions in Scala

tuned signature;

merges

More calculation-based cardinality proofs

split make_tptp_parser into two scripts, for parser and lib respectively;

added ml-yacc library sources;

added tptp parser;

merged

Structured and calculation-based proofs (with new trans rules!)

Structured and calculation-based proofs (with new trans rules!)

tuned comment;

simplified -- plain map_index is sufficient (pointed out by Enrico Tassi);

tuned;

clarified XML signature (again) -- coincide with basic Markup without explicit dependency;

more precise warning/error positions;

merged

less rigorous but more realistic migration recommendation; note on code generation of sets

tuned syntax; more candidates

tuned message (cf. ML version);

eliminated dead code; tuned;

tuned signature;

simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode);

to_pred/set attributes now properly handle variables of type "... => T set"

some recovery of IsaMakefile targets from f3c10e908f65;

added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;

added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;

added Mirabelle action info in its log file; tuned;

More mathematical symbols for ZF examples

mathematical symbols for Isabelle/ZF example theories

Using mathematical notation for <-> and cardinal arithmetic

mathematical symbols instead of ASCII

addressed a quotient-type-related issue that arose with the port to "set"

ensure no abstractions leak through after lambda-lifting (for formulas with higher-order occurrences of quantifiers)

updates for jedit-4.5.0 (still inactive);

more explicit patches;

tuned comment;

removed obsolete proper_command_at (cf. 03a2dc9e0624);

added Command.proper_range (still unused);

clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";

clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;

tuned

move test targets to test target

dropped images for importer sessions

dropped dead code

more accurate dependencies

tuned ML

dropped silly code

tuned

dropped dead code

actually add "the" Importer theory

avoid internal hol4 name references in generic importer code

generalized user-visible text

generalized attribute name

dropped dead theories

one unified Importer theory

added actual dependencies

import all importer theories in compatibility layer

merged;

dropped obsolete ROOT.ML

plugged in pre-existing theories appropriately

switch of target Import-HOL_Light-Imported: not operative at the moment

turn on quick and dirty in batch mode

tuned whitespace

file system structure separating HOL4 and HOL Light concerns

distribution of compatibility theories

formal infrastructure for import sessions

dropped dead code

tuned whitespace

spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance; spurious set/pred correction

explicit locations for import_theory and setup_theory, for better user interface conformance

discontinued obsolete Library.foldl_map and Library.apply (NB: apply = fold I);

tuned;

tuned;

tuned;

canonical argument order for attribute application;

clarified terminology of raw protocol messages;

tuned;

tuned signature -- emphasize Isabelle_Process Input vs. Output;

explicit syslog_limit reduces danger of low-level message flooding; tuned;

retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided); tuned;

clarified scope of exception handlers;

relevant timing as in ML; more PIDE modules;

more fundamental pred-to-set conversions for range and domain by means of inductive_set

merged

tuned whitespace

tuned import

dropped dead code

terminate after first exception -- avoid syslog flooding;

avoid buffer loading overrun; tuned;

merged

collecting all axioms in a locale context in quickcheck; adding some verbose output;

choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing

removing finiteness goals

adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets

Symbol.encode header edits;

merged

tuned whitespace

more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)

Removal of obsolete ML bindings

more robust locking;