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