added "dont_preplay" alias

document "dont_preplay"

tuning

implement term order attribute (for experiments)

tuning -- don't refer to old, internal version number (needlessly confusing now)

more weight attribute tuning

use TFF0 with remote Vampire, now that a newer version of Vampire has been installed there (1.8 rev. 1362) that appears to have sound support for TFF0

internal renamings

renamed E weight attribute

tuned proofs;

explicit propagation of assignment event, even if changed command set is empty; discontinued slightly odd Document_View.update_snapshot/flush_snapshot;

modernized axiomatizations;

modernized axiomatizations; tuned proofs;

updated Misc_Legacy.freeze_thaw;

discontinued remains of duplicate exception UnequalLengths (cf. 441260986b63);

moved some legacy stuff;

clarified Binding.name_of vs Name_Space.base_name vs Variable.check_name (see also 9bd8d4addd6e, 3305f573294e);

merged

merged

More structured proofs for cardinalities

merged

more structured case and induction proofs

better defaults for Metis, that seem to make it less likely to loop seemingly forever -- 0 coefficients might very well make it incomplete

allow keyword tags to be redefined, but not the command category;

further amendment of "updated" edge (cf. 6ed49c52d463) -- required for repainting of unassigned command, e.g. for inactive buffe;

clarified command span classification: strict Command.is_command, permissive Command.name;

more robust bash interpolation;

more ambitious scalac options for makedist;

less noisy Isabelle/Scala build process;

comment;

tuned;

tuned;

maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;

tuned;

tuned structure;

comments for uniformity

proper naming of simprocs according to actual target context; afford pervasive declaration which makes results available with qualified name from outside;

amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;

more precise syntax;

more antiquotations;

misc tuning to accomodate scala-2.10.0-M2;

include scala.xml as of scala-2.9.1.final/misc/scala-tool-support/jedit/modes/scala.xml -- seems to be missing in more recent distributions;

merged

merged

tidying and structured proofs

refined Local_Theory.define vs. Local_Theory.define_internal, which allows to pass alternative name to the foundational axiom -- expecially important for 'instantiation' or 'overloading', which loose name information due to Long_Name.base_name cooking etc.; actually make "raw_def" internal (cf. 80123a220219);

tuned proofs;

simultaneous read_fields -- e.g. relevant for sort assignment;

added Syntax.read_typs; tuned parallelism for syntax operations;

renamed HOL-Matrix to HOL-Matrix_LP to avoid name clash with AFP;

tuned message;

tuned proofs;

tuned proofs;

tuned exception;

merged;

spelt out missing colemmas

generalized INF_INT_eq, SUP_UN_eq

tuned specifications

sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold; tuned;

tuned grouping -- merely indicate order of magnitude;

slightly more parallel find_theorems;

'definition' no longer exports the foundational "raw_def";

some attempts to fit source on screen;

eliminated odd 'finalconsts' / Theory.add_finals;

modernized axiomatization; eliminated odd 'finalconsts';

modernized axiomatization; eliminated odd 'finalconsts';

afford strict Args.type_name (cf. 29e88714ffe4);

check declared vs. defined commands at end of session;

more abstract heading level;

less redundant data;

uniform keyword names within ML/Scala -- produce elisp names via external conversion; discontinued obsolete Keyword.thy_switch;

merged

ZF news

merged

Structured transfinite induction proofs

make more word theorems respect int/bin distinction

outer syntax command definitions based on formal command_spec derived from theory header declarations;

refute_params are given in *this* theory;

defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;

define keywords early when processing the theory header, before running the body commands;

clarified Keyword.is_keyword: union of minor and major; misc tuning and simplification;

Isabelle/jEdit supports user-defined Isar commands within the running session;

merged

beautification and structured proofs

replacing ":" by "\<in>"

Rewrote some induction proofs to be structured

more precise TPTP keywords and dependencies;

declare command keywords via theory header, including strict checking outside Pure;

prefer formally checked @{keyword} parser;

added ML antiquotation @{keyword};

declare minor keywords via theory header;

more explicit header_edits before main text_edits; handle reparses caused by syntax update;

declare keywords as side-effect of header edit; parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);

more recent recent_syntax, e.g. relevant for document rendering during startup;

clarified syntax of prospective keywords;

basic support for outer syntax keywords in theory header;

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