deactivated Datatype.distinct_simproc

dropped Datatype.distinct_simproc; tuned

order conjunctions to be printed without parentheses

approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability

merged

added add_tyconames; tuned

merged

more appropriate abstraction over distinctness rules

merged

intro_base_names combinator

merged

dropped dist_ss

merged

added is_IVar

factored out Code_Printer.aux_params

dropped rule duplicates

less non-standard combinators

nth replaces List.nth

dropped redundancy

dropped dead code

using distinct rules directly

simplified proof

dropped simproc_dist formally

tuned order of lemmas

term styles also cover antiquotations term_type and typeof

merged

lookup for datatype constructors considers type annotations to resolve overloading

added group_stmts

moved labelled_name to code_thingol

updated generated documentation

corrected syntax diagrams for styles

new generalized concept for term styles

generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles

isatest: store test identifiers

tuned proofs

added bot_boolE, top_boolI

do not use Locale.add_registration_eqs any longer

Inf/Sup now purely syntactic

merged

inf/sup1/2_iff are mere duplicates of underlying definitions: dropped

merged

added Coset as constructor

sets and cosets

added syntactic Inf and Sup

merged

New lemmas connected with the reals and infinite series

New facts about domain and range in

merged

experimental de-facto abolishment of distinctness limit

tuned handling of type variable names further

variables in type schemes must be renamed simultaneously with variables in equations

explicitly unsynchronized

explicitly unsynchronized

recovered support for Spass: re-enabled writing problems in DFG format

avoid exception Option: only apply "the" if needed

merged

atp_minimal using chain_ths again

merged

re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values

eliminated dead code; tuned;

eliminated dead code and redundant parameters; tuned;

eliminated dead code;

replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools; tuned;

replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;

Refute.refute_goal: goal addressing from 1 as usual;

Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics); command 'refute': Proof.flat_goal provides standard view on internally structured Isar goal, suitable for (semi)automated tools;

clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);

misc tuning and simplification;

macbroy2: bigger jobs first, to avoid danger of swapping during daytime;

less ambitious heap settings;

merged

merged

proper merge of interpretation equations

merged

Merged again.

Merged.

News entry: inheritance of mixins; print_interps.

Avoid administrative overhead for identity mixins.

tuned;

moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;

added Ctermtab, cterm_cache, thm_cache; tuned;

added term_cache; tuned;

Concurrently cached values.

tuned header; tuned whitespace;

core_sos_tac: SUBPROOF body operates on subgoal 1; tuned;

merged

updated generated files;

enable slow-motion mode to accomodate unsynchronized refs within theory sources;

avoid unsynchronized refs within theory sources;

explicitly Unsynchronized;

additional fixes in normarith.ML due to FuncFun and FuncUtil changes

changed core_sos_tac to use SUBPROOF

replaced and tuned uses of foldr1

tuned FuncFun and FuncUtil structure in positivstellensatz.ML

removed opening of structures

merged

merged

merged

made spass additional default prover

merged

Proved a new theorem: nat_to_nat2_inj

turned unsynchronized ref into synchronized var

merged

resolved conflict

record max lemmas used

Lazy evaluation with memoing (sequential version).

more official status of sequential implementations; tuned;

separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations;

added Task_Queue.depend (again) -- light-weight version for transitive graph; Future.join_results: record explicit dependency, detect direct task-task join cycles; Future.join_results: no change of interruptibility, allows to interrupt wait; added Future.worker_task; ThyInfo.schedule_futures: uninterruptible outer join;

handle Pattern.MATCH, not arbitrary exceptions; misc tuning, trying to reduce line length a bit;

more precise dependencies;

eliminated redundant parameters;

back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;

avoid mixed l/r infixes, which do not work in some versions of SML;

tuned;

merged

explicitly Unsynchronized

Merged.

Propagation of mixins for interpretation; reactivated diagnostic command print_interps.

Archive registrations by external view.