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