tuned signature;

clarified Named_Target.target_declaration: propagate through other levels as well; tuned signature;

Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom; Local_Theory.target refers to bottom; tuned signature;

tuned proofs

merged

tuned proof

add lemma power_le_one

tuned;

tuned signature;

more direct Local_Defs.contract; eliminated slightly odd Local_Defs.trans_term/trans_prop;

more precise Local_Defs.expand wrt. *local* prems only;

tuned comment;

more robust Scala 2.9.x interpreter invocation -- avoid separate interpreter thread and thus deadlock of Swing_Thread.now;

tuned;

dropped empty files

dropped now obsolete Cset theories

merged

tuned proofs, less guesswork;

merged

load Tools/numeral.ML in Num.thy

tuned proof

set up numeral reorient simproc in Num.thy

remove redundant simp rule

add simp rules for eve/odd on numerals

remove content-free theory ex/Arithmetic_Series_Complex.thy

rephrase lemmas about arithmetic series using numeral '2'

rephrase lemma card_Pow using '2' instead of 'Suc (Suc 0)'

replace lemmas eval_nat_numeral with a simpler reformulation

restate various simp rules for word operations using pred_numeral

new lemmas for simplifying subtraction on nat numerals

removed redundant nat-specific copies of theorems

move more theorems from Nat_Numeral.thy to Num.thy

"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);

more robust ISABELLE_JDK_HOME settings, based on exisiting JAVA_HOME provided by isatest shell environment (which depends a lot on the host);

more explicit isatest environment settings (from private .bashrc);

merged

fix search-and-replace errors

move lemma card_UNIV_bool from Nat_Numeral.thy to Finite_Set.thy

add constant pred_numeral k = numeral k - (1::nat); replace several simp rules from Nat_Numeral.thy with new ones that use pred_numeral

move lemmas from Nat_Numeral.thy to Nat.thy

move lemmas from Nat_Numeral to Int.thy and Num.thy

merged

adding theory to prove completeness of the exhaustive generators

refine bindings in quickcheck_common: do not conceal and do not declare as simps

hiding fact not so aggressively

power on predicate relations

made Mirabelle-SH's 'trivial' check optional;

merged

more specific notion of partiality (cf. Scala version);

use qualified names for rsp and rep_eq theorems in quotient_def

announcing NEWS (cf. 446cfc760ccf)

remove obsolete simp rule for powers

remove duplicate lemmas power_m1_{even,odd} in favor of power_minus1_{even,odd}

remove unneeded rewrite rules for powers of numerals

remove duplicate lemma Suc_numeral

move many lemmas from Nat_Numeral.thy to Power.thy or Num.thy

bootstrap Num.thy before Power.thy; move lemmas about powers into Power.thy

educated guess to include jdk

improved robustness with new antiquoation by Makarius

merged

updates

updated documentation files (cf. c14fda8fee38)

clarified ISABELLE_JDK_HOME: derive from running JVM, but ignore accidental JAVA_HOME; clarified jEdit/README_BUILD;

merged

removed references to obsolete theorems

merged

some tuning while reviewing the current state of the quotient_def package

improving spelling

changing more definitions to quotient_definition

removing now redundant impl_of theorems in DAList

using abstract code equations for proofs of code equations in Multiset

simplified statements and proofs;

tuned whitespace;

updated Sign.add_type, Name_Space.declare;

updated comments;

merged

remove unnecessary rules from the simpset

remove unused premises

remove duplicate lemmas

mark some duplicate lemmas for deletion

remove more redundant lemmas

tuned proofs

remove redundant lemmas

generalized lemma zpower_zmod

remove redundant lemma

remove redundant lemma

remove duplicate [algebra] declarations

generalize more div/mod lemmas

generalize some theorems about div/mod

updated to jedit-4.5.1;

merged

note a code eqn in quotient_def

dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct

more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)

fixed eta-extension of higher-order quantifiers in THF output

renamed "smt_fixed" to "smt_read_only_certificates"

tuning

tuning (in particular, Symtab instead of AList)

tweak slices, based on eval by Daniel Wand

be less forceful about ":lt" to make infinite loops less likely (could still fail with mutually recursive tail rec functions)

print a hint

avoid DL

TFF: declare free types as types

merged

association lists with distinct keys uses the quotient infrastructure to obtain code certificates; added remarks about further improvements

remove redundant lemmas

move int::ring_div instance upward, simplify several proofs

rename lemmas {divmod_int_rel_{div,mod} -> {div,mod}_int_unique, for consistency with nat lemma names

extend definition of divmod_int_rel to handle denominator=0 case

tuned proofs

shorten a proof

simplify some proofs

rename lemmas {div,mod}_eq -> {div,mod}_nat_unique, for consistency with minus_unique, inverse_unique, etc.

simplify some proofs

merged

merged

reverted to canonical name

merged

merged

revert changeset 500a5d97511a, re-enabling HOL-Proofs-Lambda

merged

fix incorrect code_modulename declarations

code lemma for function 'nat' that doesn't go into an infinite loop (fixes problem with non-terminating HOL-Proofs-Lambda)

remove old-style semicolon

merged

Functions and lemmas by Christian Sternagel

more precise treatment of \r\n as blank symbol (cf. 2bf29095d26f), e.g. relevant for loading theory headers in Isabelle/jEdit -- NB: jEdit and Isabelle/ML normalize newline variants to \n, but Isabelle/Scala retains them literally;

disabled HOL-Proofs-Lambda temporarily, which causes problems with 2a1953f0d20d;

tuned comment

merged

merged

tuned proof - no smt call

more robust command invocation via ISABELLE_JDK_HOME or SCALA_HOME (NB: bash exec requires genuine executable, not function);

updated theory header syntax and related details;

ISABELLE_JDK_HOME settings variable points to JDK with javac and jar (not just JRE); update for prospective jdk1.7.x component;

merged

reintroduced broken proofs and regenerated certificates

merged, resolving trivial conflict;

fixed Nitpick after numeral representation change (2a1953f0d20d)

merged fork with new numeral representation (see NEWS)

merged

use Thm.transfer for thms stored in generic context data storage

hide invariant constant

explicit SMTP server (appears to be required after recent change of system configuration);

more isatest subscribers;

merged

proof tidying

updated comment

resolve invariant constant name clash

update etc/isar-keywords.el

fix example files

generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem

simplified code of generation of aggregate relations

store the relational theorem for every relator

store the quotient theorem for every quotient

fix Quotient_Examples

respectfulness theorem has to be proved if a new constant is lifted by quotient_definition

adjusting to longer names in PNF_Narrowing_Engine, which was overlooked in 4106258260b3

tuned;

merged;

fixed typo

more instructive NEWS

more structured proofs

New Message

No longer treat "title" as FDL keyword

tuned proofs;

uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters); uniform treatment of target contexts as invisible; added Local_Theory.standard_form convenience;

tuned;

synchronize syntax uniformly for target stack and aux. context;

tuned;

merged

removed Satallax option, now that this is the default

doc update

improve "remote_satallax" by exploiting unsat core

generate weights and precedences for predicates as well

refinements to constructibility

More structured proofs for infinite cardinalities

actually expose target context;

more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;

tuned signature;

optional 'includes' element for long theorem statements; tuned signatures;

basic support for nested contexts including bundles; include multiple bundles; renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML); tuned signatures;

tuned messages;

basic support for nested local theory targets;

try apple.laf.useScreenMenuBar=false to make menus stay closer to the editor views they belong to -- potentially less confusing for jEdit newcomers;

improved isatest arguments for macbroy2;

clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2); tuned;

prefer explicitly qualified exception List.Empty;

merged

refined init_model: allow change of buffer name as caused by "Save as", for example; avoid init_model while buffer.isLoading -- potentially prevent NPE of getText; avoid emitting nested buffer.propertiesChanged events;

basic support for bundled declarations;

doc update

made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release

removed obsolete temporary hack

tweaks

proof tidying

minimalistic support for remote URLs: no master dir here;

optimized "metis" call

added term_order option to Mirabelle

take out experimental polymorphic @ encodings from Metis test -- proof reconstruction is fragile for them

more conservative Metis defaults, for backward compatiblity (as illustrated by one "metis" call in "Auth/KerberosV")

remove two options that were found to play hardly any role

enable "metis_advisory_simp" by default

more stats;

merged

more structured proofs

don't generate new SPASS constructs for old SPASS

tune Metis example

added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")

continued implementation of term ordering attributes

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

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;