2009-10-05 haftmann 2009-10-05 tuned handling of type variable names further
2009-10-05 haftmann 2009-10-05 variables in type schemes must be renamed simultaneously with variables in equations
2009-10-05 haftmann 2009-10-05 explicitly unsynchronized
2009-10-05 haftmann 2009-10-05 explicitly unsynchronized
2009-10-04 boehmes 2009-10-04 recovered support for Spass: re-enabled writing problems in DFG format
2009-10-04 boehmes 2009-10-04 avoid exception Option: only apply "the" if needed
2009-10-04 nipkow 2009-10-04 merged
2009-09-30 Philipp Meyer 2009-09-30 atp_minimal using chain_ths again
2009-10-03 boehmes 2009-10-03 merged
2009-10-03 boehmes 2009-10-03 re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values, eliminated unused provers, turned references into configuration values
2009-10-02 wenzelm 2009-10-02 eliminated dead code; tuned;
2009-10-02 wenzelm 2009-10-02 eliminated dead code and redundant parameters; tuned;
2009-10-02 wenzelm 2009-10-02 eliminated dead code;
2009-10-02 wenzelm 2009-10-02 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools; tuned;
2009-10-02 wenzelm 2009-10-02 replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-02 wenzelm 2009-10-02 Refute.refute_goal: goal addressing from 1 as usual;
2009-10-02 wenzelm 2009-10-02 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;
2009-10-02 wenzelm 2009-10-02 clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-10-02 wenzelm 2009-10-02 misc tuning and simplification;
2009-10-02 wenzelm 2009-10-02 macbroy2: bigger jobs first, to avoid danger of swapping during daytime;
2009-10-02 wenzelm 2009-10-02 less ambitious heap settings;
2009-10-02 haftmann 2009-10-02 merged
2009-10-01 haftmann 2009-10-01 merged
2009-10-01 haftmann 2009-10-01 proper merge of interpretation equations
2009-10-02 wenzelm 2009-10-02 merged
2009-10-01 ballarin 2009-10-01 Merged again.
2009-10-01 ballarin 2009-10-01 Merged.
2009-10-01 ballarin 2009-10-01 News entry: inheritance of mixins; print_interps.
2009-10-01 ballarin 2009-10-01 Avoid administrative overhead for identity mixins.
2009-10-01 wenzelm 2009-10-01 tuned;
2009-10-01 wenzelm 2009-10-01 moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
2009-10-01 wenzelm 2009-10-01 added Ctermtab, cterm_cache, thm_cache; tuned;
2009-10-01 wenzelm 2009-10-01 added term_cache; tuned;
2009-10-01 wenzelm 2009-10-01 Concurrently cached values.
2009-10-01 wenzelm 2009-10-01 tuned header; tuned whitespace;
2009-10-01 wenzelm 2009-10-01 core_sos_tac: SUBPROOF body operates on subgoal 1; tuned;
2009-10-01 wenzelm 2009-10-01 merged
2009-10-01 wenzelm 2009-10-01 updated generated files;
2009-10-01 wenzelm 2009-10-01 enable slow-motion mode to accomodate unsynchronized refs within theory sources;
2009-10-01 wenzelm 2009-10-01 avoid unsynchronized refs within theory sources;
2009-10-01 wenzelm 2009-10-01 explicitly Unsynchronized;
2009-10-01 Philipp Meyer 2009-10-01 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
2009-10-01 Philipp Meyer 2009-10-01 changed core_sos_tac to use SUBPROOF
2009-09-30 Philipp Meyer 2009-09-30 replaced and tuned uses of foldr1
2009-09-30 Philipp Meyer 2009-09-30 tuned FuncFun and FuncUtil structure in positivstellensatz.ML
2009-09-22 Philipp Meyer 2009-09-22 removed opening of structures
2009-10-01 wenzelm 2009-10-01 merged
2009-10-01 nipkow 2009-10-01 merged
2009-10-01 nipkow 2009-10-01 merged
2009-10-01 nipkow 2009-10-01 made spass additional default prover
2009-10-01 paulson 2009-10-01 merged
2009-10-01 paulson 2009-10-01 Proved a new theorem: nat_to_nat2_inj
2009-10-01 boehmes 2009-10-01 turned unsynchronized ref into synchronized var
2009-10-01 nipkow 2009-10-01 merged
2009-10-01 nipkow 2009-10-01 resolved conflict
2009-10-01 nipkow 2009-10-01 record max lemmas used
2009-10-01 wenzelm 2009-10-01 Lazy evaluation with memoing (sequential version).
2009-10-01 wenzelm 2009-10-01 more official status of sequential implementations; tuned;
2009-10-01 wenzelm 2009-10-01 separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations;
2009-10-01 wenzelm 2009-10-01 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;