isabelle: Graph

ATP_Manager.get_prover: canonical argument order;
2009-10-15, by wenzelm
tuned proof (via atp_minimized);
2009-10-15, by wenzelm
sort_strings (cf. Pure/library.ML);
2009-10-15, by wenzelm
clarified File.platform_path vs. File.shell_path;
2009-10-15, by wenzelm
exported File.shell_quote;
2009-10-15, by wenzelm
misc tuning and recovery of Isabelle coding style;
2009-10-15, by wenzelm
eliminated extraneous wrapping of public records;
2009-10-15, by wenzelm
tuned signature;
2009-10-15, by wenzelm
renamed functor HeapFun to Heap;
2009-10-15, by wenzelm
misc tuning and clarification;
2009-10-15, by wenzelm
structure ATP_Manager: eliminated slightly odd get/set operations in favour of Unsynchronized.ref;
2009-10-15, by wenzelm
modernized structure names;
2009-10-14, by wenzelm
show direct GC time (which is included in CPU time);
2009-10-14, by wenzelm
eliminated obsolete C/flip combinator;
2009-10-14, by wenzelm
added List.nth
2009-10-14, by nipkow
tuned make parameters for sunbroy2;
2009-10-14, by wenzelm
accomodate old version of "tail", e.g. on sunbroy2;
2009-10-14, by wenzelm
settings for parallel experimental Poly/ML 5.3;
2009-10-14, by wenzelm
sharpened name
2009-10-14, by haftmann
more explicit notion of canonized code equations
2009-10-14, by haftmann
more explicit notion of canonized code equations
2009-10-14, by haftmann
tuned whitespace
2009-10-14, by haftmann
tuned whitespace
2009-10-14, by haftmann
dropped Code_Printer prefix where feasible; fixed whitespace issues; more coherent terminology
2009-10-14, by haftmann
merged
2009-10-13, by haftmann
deactivated Datatype.distinct_simproc
2009-10-13, by haftmann
dropped Datatype.distinct_simproc; tuned
2009-10-13, by haftmann
order conjunctions to be printed without parentheses
2009-10-13, by hoelzl
approximation now fails earlier when using interval splitting; value [approximate] now supports bounded variables; renamed Var -> Atom for better readability
2009-10-13, by hoelzl
merged
2009-10-13, by haftmann
added add_tyconames; tuned
2009-10-12, by haftmann
merged
2009-10-13, by haftmann
more appropriate abstraction over distinctness rules
2009-10-13, by haftmann
merged
2009-10-12, by haftmann
intro_base_names combinator
2009-10-12, by haftmann
merged
2009-10-12, by haftmann
dropped dist_ss
2009-10-12, by haftmann
merged
2009-10-12, by haftmann
added is_IVar
2009-10-12, by haftmann
factored out Code_Printer.aux_params
2009-10-12, by haftmann
dropped rule duplicates
2009-10-12, by haftmann
less non-standard combinators
2009-10-12, by haftmann
nth replaces List.nth
2009-10-12, by haftmann
dropped redundancy
2009-10-12, by haftmann
dropped dead code
2009-10-12, by haftmann
using distinct rules directly
2009-10-12, by haftmann
simplified proof
2009-10-09, by haftmann
dropped simproc_dist formally
2009-10-09, by haftmann
tuned order of lemmas
2009-10-09, by haftmann
term styles also cover antiquotations term_type and typeof
2009-10-09, by haftmann
merged
2009-10-09, by haftmann
lookup for datatype constructors considers type annotations to resolve overloading
2009-10-08, by haftmann
added group_stmts
2009-10-08, by haftmann
moved labelled_name to code_thingol
2009-10-08, by haftmann
updated generated documentation
2009-10-08, by haftmann
corrected syntax diagrams for styles
2009-10-08, by haftmann
new generalized concept for term styles
2009-10-08, by haftmann
generalized term styles: transformations may depend on arguments; modernized term_style module; antiquotations thm, prop and term accepting term styles
2009-10-07, by haftmann
isatest: store test identifiers
2009-10-08, by krauss
tuned proofs
2009-10-07, by haftmann
added bot_boolE, top_boolI
2009-10-07, by haftmann
do not use Locale.add_registration_eqs any longer
2009-10-07, by haftmann
Inf/Sup now purely syntactic
2009-10-07, by haftmann
merged
2009-10-06, by haftmann
inf/sup1/2_iff are mere duplicates of underlying definitions: dropped
2009-10-06, by haftmann
merged
2009-10-06, by haftmann
added Coset as constructor
2009-10-06, by haftmann
sets and cosets
2009-10-06, by haftmann
added syntactic Inf and Sup
2009-10-06, by haftmann
merged
2009-10-05, by paulson
New lemmas connected with the reals and infinite series
2009-10-05, by paulson
New facts about domain and range in
2009-10-05, by paulson
merged
2009-10-05, by haftmann
experimental de-facto abolishment of distinctness limit
2009-10-05, by haftmann
tuned handling of type variable names further
2009-10-05, by haftmann
variables in type schemes must be renamed simultaneously with variables in equations
2009-10-05, by haftmann
explicitly unsynchronized
2009-10-05, by haftmann
explicitly unsynchronized
2009-10-05, by haftmann
recovered support for Spass: re-enabled writing problems in DFG format
2009-10-04, by boehmes
avoid exception Option: only apply "the" if needed
2009-10-04, by boehmes
merged
2009-10-04, by nipkow
atp_minimal using chain_ths again
2009-09-30, by Philipp Meyer
merged
2009-10-03, by boehmes
re-organized signature of AtpWrapper structure: records instead of unnamed parameters and return values,
2009-10-03, by boehmes
eliminated dead code;
2009-10-02, by wenzelm
eliminated dead code and redundant parameters;
2009-10-02, by wenzelm
eliminated dead code;
2009-10-02, by wenzelm
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-02, by wenzelm
replaced Proof.get_goal state by Proof.flat_goal state, which provides the standard view on goals for (semi)automated tools;
2009-10-02, by wenzelm
Refute.refute_goal: goal addressing from 1 as usual;
2009-10-02, by wenzelm
Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
2009-10-02, by wenzelm
clarified Proof.refine_insert -- always "refine" to apply standard method treatment (of conjunctions);
2009-10-02, by wenzelm
misc tuning and simplification;
2009-10-02, by wenzelm
macbroy2: bigger jobs first, to avoid danger of swapping during daytime;
2009-10-02, by wenzelm
less ambitious heap settings;
2009-10-02, by wenzelm
merged
2009-10-02, by haftmann
merged
2009-10-01, by haftmann
proper merge of interpretation equations
2009-10-01, by haftmann
merged
2009-10-02, by wenzelm
Merged again.
2009-10-01, by ballarin
Merged.
2009-10-01, by ballarin
News entry: inheritance of mixins; print_interps.
2009-10-01, by ballarin
Avoid administrative overhead for identity mixins.
2009-10-01, by ballarin
tuned;
2009-10-01, by wenzelm
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
2009-10-01, by wenzelm
added Ctermtab, cterm_cache, thm_cache;
2009-10-01, by wenzelm
added term_cache;
2009-10-01, by wenzelm
Concurrently cached values.
2009-10-01, by wenzelm
tuned header;
2009-10-01, by wenzelm
core_sos_tac: SUBPROOF body operates on subgoal 1;
2009-10-01, by wenzelm
merged
2009-10-01, by wenzelm
updated generated files;
2009-10-01, by wenzelm
enable slow-motion mode to accomodate unsynchronized refs within theory sources;
2009-10-01, by wenzelm
avoid unsynchronized refs within theory sources;
2009-10-01, by wenzelm
explicitly Unsynchronized;
2009-10-01, by wenzelm
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
2009-10-01, by Philipp Meyer
changed core_sos_tac to use SUBPROOF
2009-10-01, by Philipp Meyer
replaced and tuned uses of foldr1
2009-09-30, by Philipp Meyer
tuned FuncFun and FuncUtil structure in positivstellensatz.ML
2009-09-30, by Philipp Meyer
removed opening of structures
2009-09-22, by Philipp Meyer
merged
2009-10-01, by wenzelm
merged
2009-10-01, by nipkow
merged
2009-10-01, by nipkow
made spass additional default prover
2009-10-01, by nipkow
merged
2009-10-01, by paulson
Proved a new theorem: nat_to_nat2_inj
2009-10-01, by paulson
turned unsynchronized ref into synchronized var
2009-10-01, by boehmes
merged
2009-10-01, by nipkow
resolved conflict
2009-10-01, by nipkow
record max lemmas used
2009-10-01, by nipkow
Lazy evaluation with memoing (sequential version).
2009-10-01, by wenzelm
more official status of sequential implementations;
2009-10-01, by wenzelm
separate concurrent/sequential versions of lazy evaluation;
2009-10-01, by wenzelm
added Task_Queue.depend (again) -- light-weight version for transitive graph;
2009-10-01, by wenzelm
handle Pattern.MATCH, not arbitrary exceptions;
2009-10-01, by wenzelm
more precise dependencies;
2009-10-01, by wenzelm
eliminated redundant parameters;
2009-10-01, by wenzelm
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;
2009-10-01, by wenzelm
avoid mixed l/r infixes, which do not work in some versions of SML;
2009-10-01, by wenzelm
tuned;
2009-10-01, by wenzelm
merged
2009-10-01, by wenzelm
explicitly Unsynchronized
2009-10-01, by haftmann
Merged.
2009-10-01, by ballarin
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-09-29, by ballarin
Archive registrations by external view.
2009-09-27, by ballarin
Stricter test: raise error if registration generates duplicate theorem.
2009-09-26, by ballarin
Explicit management of registration mixins.
2009-09-19, by ballarin
Improved comments and api names.
2009-08-19, by ballarin
eliminated dead code, redundant bindings and parameters;
2009-10-01, by wenzelm
misc tuning and simplification;
2009-10-01, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
Sorts.of_sort_derivation: no pp here;
2009-09-30, by wenzelm
eliminated redundant bindings;
2009-09-30, by wenzelm
actually perform Isar_Document.init on startup;
2009-09-30, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
removed dead code;
2009-09-30, by wenzelm
handle Type.TYPE_MATCH, not arbitrary exceptions;
2009-09-30, by wenzelm
removed redundant Sign.certify_prop, use Sign.cert_prop instead;
2009-09-30, by wenzelm
PARALLEL_GOALS: proper scope for exception FAILED, with dummy argument to prevent its interpretation as variable;
2009-09-30, by wenzelm
actually export unit parser;
2009-09-30, by wenzelm
eliminated dead code;
2009-09-30, by wenzelm
eliminated redundant parameters;
2009-09-30, by wenzelm
eliminated redundant bindings;
2009-09-30, by wenzelm
merged
2009-09-30, by haftmann
moved lemmas about sup on bool to Lattices.thy
2009-09-30, by haftmann
moved lemmas about sup on bool to Lattices.thy
2009-09-30, by haftmann
tuned proofs
2009-09-30, by haftmann
tuned headings
2009-09-30, by haftmann
report unreferenced ids;
2009-09-30, by wenzelm
tuned whitespace;
2009-09-30, by wenzelm
more uniform treatment of structure Unsynchronized in ML bootstrap phase;
2009-09-30, by wenzelm
merged
2009-09-30, by haftmann
mandatory prefix where appropriate
2009-09-30, by haftmann
mandatory prefix where appropriate
2009-09-30, by haftmann
tuned whitespace
2009-09-30, by haftmann
replaced chained_goal by slightly more appropriate flat_goal;
2009-09-30, by wenzelm
made SML/NJ happy;
2009-09-30, by wenzelm
added chained_goal, which presents the goal thm as seen by semi-structured methods;
2009-09-30, by wenzelm
tuned;
2009-09-29, by wenzelm
removed dead/duplicate code;
2009-09-29, by wenzelm
aliases for Thomas Sewell;
2009-09-29, by wenzelm
modernized Balanced_Tree;
2009-09-29, by wenzelm
replaced meta_iffD2 by existing Drule.equal_elim_rule2;
2009-09-29, by wenzelm
tuned header;
2009-09-29, by wenzelm
Thomas Sewell, NICTA: more efficient HOL/record implementation;
2009-09-29, by wenzelm
tuned whitespace -- recover basic Isabelle conventions;
2009-09-29, by wenzelm
merged
2009-09-29, by wenzelm
Merge with isabelle dev changes.
2009-09-29, by Thomas Sewell
Replace OldTerm.term_vars with Term.add_vars in named_cterm_instantiate.
2009-09-29, by Thomas Sewell
Avoid a possible variable name conflict in instantiating a theorem.
2009-09-28, by Thomas Sewell
Fix unescaped expressions breaking latex output in Record.thy
2009-09-28, by Thomas Sewell
Merge record patch with updates from isabelle mainline.
2009-09-28, by Thomas Sewell
Avoid record-inner constants in polymorphic definitions in Bali
2009-09-25, by Thomas Sewell
Merge with changes from isabelle dev repository.
2009-09-24, by Thomas Sewell
Initial response to feedback from Norbert, Makarius on record patch
2009-09-23, by tsewell
Branch merge for isabelle mainline updates.
2009-09-22, by Thomas Sewell
Branch merge with updates from mainline isabelle.
2009-09-17, by Thomas Sewell
Implement previous fix (don't duplicate ext_def) correctly.
2009-09-11, by Thomas Sewell
There's no particular reason to duplicate the extension
2009-09-11, by Thomas Sewell
Merged with mainline changes.
2009-09-11, by Thomas Sewell
Adjust some documentation.
2009-09-11, by Thomas Sewell
Simplification of various aspects of the IsTuple component
2009-09-10, by Thomas Sewell
Record patch imported and working.
2009-09-10, by Thomas Sewell
Initial attempt at porting record update to repository Isabelle.
2009-08-27, by tsewell
Synchronized and Unsynchronized;
2009-09-29, by wenzelm
hide "ref" by default, to enforce excplicit indication as Unsynchronized;
2009-09-29, by wenzelm
explicit indication of Unsynchronized.ref;
2009-09-29, by wenzelm
open_unsynchronized for interactive Isar loop;
2009-09-29, by wenzelm
explicit indication of Unsynchronized.ref;
2009-09-29, by wenzelm
Raw ML references as unsynchronized state variables.
2009-09-29, by wenzelm
Dummy version of state variables -- plain refs for sequential access.
2009-09-28, by wenzelm
reactivated at-sml-dev-e;
2009-09-28, by wenzelm
misc tuning and modernization;
2009-09-28, by wenzelm
moved generic cong_tac from HOL/Tools/datatype_aux.ML to Tools/cong_tac.ML, proper subgoal selection (failure, not exception);
2009-09-28, by wenzelm
merged
2009-09-28, by wenzelm
less auxiliary functions
2009-09-28, by haftmann
tuned
2009-09-28, by haftmann
shared code between rep_datatype and datatype
2009-09-28, by haftmann
further unification of datatype and rep_datatype
2009-09-28, by haftmann
avoid compound fields in datatype info record
2009-09-28, by haftmann
fold_body_thms: pass pthm identifier;
2009-09-28, by wenzelm
tuned internal source structure;
2009-09-28, by wenzelm
added fork_deps_pri;
2009-09-28, by wenzelm
merged
2009-09-28, by haftmann
explicit pointless checkpoint
2009-09-28, by haftmann
emerging common infrastructure for datatype and rep_datatype
2009-09-27, by haftmann
streamlined rep_datatype further
2009-09-27, by haftmann
simplified rep_datatype
2009-09-27, by haftmann
more appropriate order of field in dt_info
2009-09-27, by haftmann
re-established reasonable inner outline for module
2009-09-27, by haftmann
merged
2009-09-27, by wenzelm
adjusted to changes in datatype package
2009-09-27, by haftmann
merged
2009-09-27, by haftmann
dropped dead code
2009-09-27, by haftmann
registering split rules and projected induction rules; ML identifiers more close to Isar theorem names
2009-09-27, by haftmann
fold_body_thms/join_bodies: explicitly check for cyclic theorem references;
2009-09-27, by wenzelm
tuned;
2009-09-27, by wenzelm
reachable: recovered reverse post-order (lost in 73ad4884441f), which is expected for all_preds/all_succs and required for topological_order;
2009-09-27, by wenzelm
merged
2009-09-25, by paulson