plain non-dependent types;

turned IsarDocument into trait for IsabelleProcess;

HOL_USEDIR_OPTIONS: -Q false, giving up parallel proofs for now due to memory shortage;

thm_proof: recovered single-threaded version;

merged

recovered example types from WordMain.thy;

merged

added share_common_data -- reduces heap space, but takes long;

use https;

thm_proof: replaced lazy by composed futures;

proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;

explicit constraints

entry point for Word library now named Word

fixed reading of class specs: declare class operations in context

stripped Id

streamlined definitions, executable equality

tuned header

entry point for Word library now named Word

correct proof of assm_intro rule

sorted_take, sorted_drop

merged

fixed fixme

avoiding misleading name duplicate

lemmas dom_const, dom_if

merged

moved all output to watcher-thread

be more liberal with selected code statements

making SMLNJ happy

tuned signature;

binding replaces Binding.T

binding replaces bstring

simplified handling of base sort, dropped axclass

dropped print_interps

binding replaces bstring

merged

allow empty class specs

changed import hierarchy

no base sort in class import

updated generated files;

removed Ids;

eliminated obsolete var morphism;

eliminated obsolete var morphism; tuned;

eliminated obsolete var morphism; simplified map_ctxt: just one version, without var; removed obsolete params_of, prems_of, facts_of; removed obsolete rename operations; tuned;

merged

tuned whitespace;

merged

removed vampire-wrapper (remote-script covers that)

2 provers

tuned; really find failure

do not interrupt successful thread

cancel whole group

Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip

pass timeout to prover; especially to remote-script

typo

merged

modified remote script; modified handling of errors

Automated merge with http://isabelle.in.tum.de/repos/isabelle/tip

removed useless

simplified usage of remote-script; added compatible remote-atps

dropped print_interps

binding replaces bstring

merged

merged

binding replaces bstring

binding is alias for Binding.T

dropped ID

binding replaces bstring

refined witness algebra

code cleanup

wrecked old locale package and related modules

improved and corrected reading of class specs -- still draft version

tuned

tuned;

replaced java.util.Properties by plain association list; added parse_message;

replaced java.util.Properties by plain association list; tuned;

IsabelleSystem: provide Symbol.Interpretation;

more general init of Symbol.Interpretation, independent of IsabelleSystem instance;

more robust handling of quick_and_dirty;

Merged, overriding earlier fix.

Fixed tutorial to compile with new locales; grammar of new locale commands.

removed Ids;

removed Ids;

intern names of elements and attributes;

merged

lcp = paulson

"code equation" replaces "defining equation"

tuned

improved tackling of subclasses

tuned proof

smart path detection

corrected user aliases

added churn script

Scala wrapper for interactive Isar documents;

added append_list, encode_list; tuned;

join_results: when dependencies are resulved (but not finished yet), always continue execution as worker thread -- improved parallelism at the cost of some reactivity;

with_attributes: make double sure that unsafe attributes are avoided;

bug fixes

bug fixes

improved calculation of morphisms and rules

merged

tuned signature

exported depedencies; tuned signature

merged

merged

use match_tac instead of resolve_tac for continuity simproc

more instance declarations for poly

add lemmas about degree

rename plength to psize

rename divmod_poly to pdivmod

merged.

add strictness and compactness lemmas to Product_Cpo.thy

rename Dsum.thy to Sum_Cpo.thy

minimize dependencies

add lemmas cont2monofunE, cont2cont_apply

add Product_Cpo.thy

change to simpler, more extensible continuity simproc define attribute [cont2cont] for continuity rules; new continuity simproc just applies cont2cont rules repeatedly; split theory Product_Cpo from Cprod, so Cfun can import Product_Cpo; add lemma cont2cont_LAM', which is suitable as a cont2cont rule.

merged

bug fix

merged

code cleanup

explicit equation morphism

close derivation of classrels

no document for HOL-Base

moved message markup into Scala layer -- reduced redundancy;

added parse_body_failsafe;

define_state: use empty_state; edit_document: report_updates before running commands; tuned;

provide end_document;

merged

run command: check theory name for init; tuned;

run_command: check theory name for init;

export check_name;

fixed location of Imperative_HOL

adapted to changes in class package

merged

migrated class package to new locale implementation

corrected preparation of instances: parameters are proper names, not raw terms

migrated class package to new locale implementation

merged

fold_entries: non-optional start, permissive; renamed find_entries to first_entry, tuned; update_state: run as state_id'; update_states: symmetric changes;

Result.toString: XML output of status messages;

added HOL-Base image

moved Univ_Poly to Library

merged

tuned

added cert_read_declaration; more exports; tuned signature

merged

command 'Isar.edit_document': actually invoke edit_document;

merged

fixed error message spacing

tuned interpretation code

tuned

type constraints and sort intersection

dropped $Id$

decativate Toplevel.debug after reading

exported break reference

tuned;

edit_document: proper edits/edit markup, including the document id; tuned;

replaced command_state by edits/edit;

removed junk;

merged

one more [code del] declaration

misc cleanup and simplification;

added run_command (from isar_document.ML); tuned;

added command_state markup;

tuned ASCII art;

declare pCons_0_0 [code post]

merged

code generation for polynomials

merged

more [code del] declarations

declare more definitions [code del]

define polynomial multiplication using poly_rec

merged.

declare smult rules [simp]

simplify proof of coeff_mult_degree_sum

convert Deriv.thy to use new Polynomial library (incomplete)

Integration imports ATP_Linkup (for metis)

misc internal rearrangements; fold_entries: really start from start, or optional position; added find_first_entries, find_first_entries; insert_entry: always invalidate next state; added refresh_states (partial version);

replaced sys_error by plain error; some basic operations on command entries within a document;

merged

change dvd_minus_iff, minus_dvd_iff from [iff] to [simp] (due to problems with Library/Primes.thy)

convert Fundamental_Theorem_Algebra.thy to use new Polynomial library

add Polynomial.thy to makefile

add lemmas poly_power, poly_roots_finite

declare dvd_minus_iff and minus_dvd_iff [iff]

new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]

added Isar/isar_document.ML: Interactive Isar documents.

export list;

correctness and uniqueness of synthetic division

add synthetic division algorithm for polynomials

add list-style syntax for pCons

add recursion combinator poly_rec; define poly function using poly_rec

add lemmas degree_{add,diff}_less

merged

new theory of polynomials

tuned categories;

added outer_keyword.scala: Isar command keyword classification;

added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;

load main entry points sequentially, for reduced memory demands;

merged

merged

less ambitious ML_OPTIONS;

merged

merged

explicit bookkeeping of intro rules and axiom

stripped Id

construct explicit class morphism

less ambitious ML_OPTIONS;

schedule_futures: save memory for non-parallel proofs, by applying after_load as soon as possible here;

future_result: avoid expensive norm_proof (consider usedir option -Q false in low-memory situations);

added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;

remove_thy: perform PureThy.cancel_proofs; schedule_futures: PureThy.join_proofs before after_load -- achieves parallel error messages;

added cancel_proofs, based on task groups of "entered" proofs;

added pending_groups -- accumulates task groups of local derivations only;

added cancel_group;

merged

schedule_futures: tuned final consolidation, explicit after_load phase;

load_thy: explicit after_load phase for presentation;

excursion: commit_exit internally -- checkpoints are fully persistent now; excursion: do not force intermediate result states yet -- great performance improvement;

slightly more robust matching of session name;

merged

fixed proof involving dvd;

tuned;

added force_result;

use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in post-hoc fashion;

simplified join_proofs;

merged

added split_thy_path;

added running task markup;

tuned;

merged

merged

merged.

fix proof broken by changes in dvd theory

merged.

remove type-specific proofs

add lemma dvd_diff to class comm_ring_1

add lemmas dvd_minus_iff and minus_dvd_iff in class comm_ring_1

move lemmas mult_minus{left,right} inside class ring

clean up division_ring proofs

add class ring_div; generalize mod/diff/minus proofs for class ring_div

generalize zmod_zmod_cancel -> mod_mod_cancel

generalize some div/mod lemmas; remove type-specific proofs

add tracing for domain package proofs

rename abbreviation square -> power2, to match theorem names

merged

split of Imperative_HOL theories from HOL-Library

NEWS and CONTRIBUTORS

dded code_thm antiquotation

made SML/NJ happy

merged

merged

tuned siganture of locale.ML

tuned signature; internal code reorganisation

tuned signature; changed locale predicate name convention

changed locale predicate name convention

inductive: added fork_mono flag;

added fork_mono flag, which is usually enabled in batch-mode only; mono rule: unnamed LocalTheory.node ensures proper joining of pending proofs;

Proof.global_future_terminal_proof;

Proof.global_future_proof;

future_proof: refined version covers local_future_proof and global_future_proof; future_proof: refrain from full Variable.auto_fixes -- not all contexts in the stack are in body mode; refined is_relevant: mode check; added local/global_future_terminal_proof;

more robust propagation of errors through bulk jobs;

qed/after_qed: singleton result;

Proof.future_terminal_proof: no fork for interactive mode -- proofs need to be checked immediately here;

future_terminal_proof: no fork for interactive mode, assert_backward;

added local_theory';

merged

proper local_theory after Class.class

more parallel loading;

more parallel loading;

merged

merged.

make cont_proc handle eta-contracted terms

implement is_closed_term using Term.loose_bvar

use Thm.close_derivation instead of standard

tuned;

merged

renamed structure ParList to Par_List;

parallelized merge_data;

tuned map: reduced overhead due to bulk jobs; tuned join_results: reduced overhead for finished futures; tuned;

added is_valid; added extend: support bulk jobs; tuned;

future_terminal_proof: check Future.enabled;

merged

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

locale -> old_locale, new_locale -> locale

removed locale adaption layer

rearranged target theories

removed locale adaption layer

merged

misc tuning and modernization;

merged.

add lemma psize_unique; simplify some proofs

minimize imports

parallelize some internal proofs via Proof.future_terminal_proof;

added future_terminal_proof;

Isar.init;

simplified tty model -- back to plain list history, which is independent of editor model;

added is_control, is_regular, is_theory_begin;

more precise is_relevant: requires original main goal, not initial goal state; tuned future_proof: minimal modification of goal state, retain original maxidx; tuned;

tuned protect, conclude: Drule.comp_no_flatten;

added comp_no_flatten;

future proofs: back to Future.fork_pri ~1 for improved parallelism;

cancel: unique threads;

more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;

added eq_group; opaque signature match prevents accidental task/group equality; added cancel_all;

merged

separator, is_qualified

added instance for bot, top

added binding.ML

merged

merged

improved boostrap order: theory_target.ML before expression.ML

named code theorem for Fract_norm

tuned settings;

merged

removed references to OldTerm.*

tuned message_text;

removed obsolete XML mode; tuned comments; tuned;

xsymbols: use plain Symbol.output; explicit rendering of message body: print mode is always YXML, markup is only observed for singleton text (avoids overlap of inner tokens with certain status messages), test XML markup is outermost (allows Proof General font-lock); Markup.no_output;

Markup.no_output;

added output; improved encode_raw: map empty to empty; tuned;

removed unused add_substring; back to simple list implementation;

renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;

removed print mode "PGASCII" -- 7-bit ASCII communication now always enabled;

updated rendering of inner token markup;

more detailed inner token markup;

added numeral, which supercedes num, xnum, float; renamed xstr to inner_string;

renamed token markup "_xstr" to "_inner_string";

removed dead code; proper "_numeral" token markup; proper printing of arguments (higher-order numerals);

renamed ThyEdit (in thy_edit.ML) to ThySyntax (in thy_syntax.ML);

tuned;

Isar.command: plain Position.id; tuned;

added type 'a parser, simplified signature;

added type 'a parser, simplified signature; added internal_command wrapper; tuned;

added type 'a parser, simplified signature; moved properties to value_parse.ML; moved props_text to isar_syn.ML;

added props_text (from outer_parse.ML);

added Isar/value_parse.ML: Outer syntax parsers for basic ML values.

added id; tuned;

MetaSimplifier.SIMPLIFIER;

fixed assumption proof;

tuned header and description of boot files;

merged;

normalized some ML type/val aliases;

assumption/close: discontinued implicit prems;

avoid implicit use of prems;

updated generated files;

eliminated implicit use of prems; unified fact names: a, b, ab;

updated generated files;

updated type 'a lazy; proper name for type simpset;

proper import of ~~/src/HOL/ex/ReflectedFerrack;

crude adaption to intermediate class/locale version;

crude adaption to new locales;

avoid implicit prems -- tuned proofs;

avoid implicit use of prems;

Term.add_consts;

eliminated OldTerm.(add_)term_consts; eliminated polymorphic version of insert;

avoid polymorphic equality;

eliminated OldTerm.(add_)term_consts;

added canonical add_const_names, add_consts;

provide structure CharVector;

isabelle-process; provide structure Word; provide IntInf.log2;

updated sessions;

removed unused add_term_free_names;

eliminated OldTerm.add_term_free_names;

updated header;

Term.declare_typ_names, Term.declare_term_frees;

added declare_term_frees; tuned signature;

Term.declare_term_frees;

qualified Term.rename_wrt_term;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.;

use fold_aterms directly;

use exists_Const directly;

use regular Term.add_XXX etc.;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use exists_Const directly;

moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;

use exists_subterm directly; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use exists_subterm directly;

use regular Term.add_vars, Term.add_frees etc.; moved old add_term_vars, add_term_frees etc. to structure OldTerm;

moved old add_term_vars, add_term_frees etc. to structure OldTerm;

use regular Term.add_vars, Term.add_frees etc.;

added old_term.ML;

Some old-style term operations.