isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

back: Toplevel.actual/skip_proof;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
renamed set_context to context;
2005-10-18, by wenzelm
functor: no Simplifier argument;
2005-10-18, by wenzelm
moved helper lemma to HilbertChoice.thy;
2005-10-18, by wenzelm
Simplifier.theory_context;
2005-10-18, by wenzelm
added lemma exE_some (from specification_package.ML);
2005-10-18, by wenzelm
Simplifier.theory_context;
2005-10-18, by wenzelm
tuned error msg;
2005-10-18, by wenzelm
Simplifier.context/theory_context;
2005-10-18, by wenzelm
updated;
2005-10-18, by wenzelm
new interface to make_conjecture_clauses
2005-10-18, by paulson
* Simplifier: simpset of a running simplification process contains a proof context;
2005-10-17, by wenzelm
added type_solver (uses Simplifier.the_context);
2005-10-17, by wenzelm
added pos/negDivAlg_induct declarations (from Main.thy);
2005-10-17, by wenzelm
moved pos/negDivAlg_induct declarations to Integ/IntDiv.thy;
2005-10-17, by wenzelm
removed obsolete/experimental context components (superceded by Simplifier.the_context);
2005-10-17, by wenzelm
added set/addloop' for simpset dependent loopers;
2005-10-17, by wenzelm
functor: no Simplifier argument;
2005-10-17, by wenzelm
change_claset(_of): more abtract interface;
2005-10-17, by wenzelm
functor: no Simplifier argument;
2005-10-17, by wenzelm
tuned;
2005-10-17, by wenzelm
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-10-17, by wenzelm
change_claset/simpset;
2005-10-17, by wenzelm
change_claset/simpset;
2005-10-17, by wenzelm
Improved proof of injectivity theorems to make it work on
2005-10-17, by berghofe
Fixed bug in proof of support theorem (it failed on constructors with no arguments).
2005-10-17, by berghofe
Implemented proofs for support and freshness theorems.
2005-10-17, by berghofe
deleted leading space in the definition of fresh
2005-10-17, by urbanc
Initial revision.
2005-10-17, by berghofe
tuned;
2005-10-15, by wenzelm
tuned comment;
2005-10-15, by wenzelm
added ML_type, ML_struct;
2005-10-15, by wenzelm
more;
2005-10-15, by wenzelm
* antiquotations ML_type, ML_struct;
2005-10-15, by wenzelm
added guess;
2005-10-15, by wenzelm
added antiquotations ML_type, ML_struct;
2005-10-15, by wenzelm
use perl for test/stat;
2005-10-15, by wenzelm
export strip_params;
2005-10-15, by wenzelm
note_thmss, read/cert_vars etc.: natural argument order;
2005-10-15, by wenzelm
goal statements: before_qed argument;
2005-10-15, by wenzelm
added 'guess', which derives the obtained context from the course of reasoning;
2005-10-15, by wenzelm
added primitive_text, succeed_text;
2005-10-15, by wenzelm
goal statements: accomodate before_qed argument;
2005-10-15, by wenzelm
goal statements: accomodate before_qed argument;
2005-10-15, by wenzelm
added 'guess';
2005-10-15, by wenzelm
tuned;
2005-10-15, by wenzelm
added no_facts;
2005-10-15, by wenzelm
tuned comments;
2005-10-15, by wenzelm
updated;
2005-10-15, by wenzelm
signature changes
2005-10-14, by paulson
added module rat.ML for rational numbers
2005-10-14, by haftmann
longer time out for test (kleing)
2005-10-14, by isatest
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-14, by paulson
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
2005-10-14, by paulson
obsolete;
2005-10-13, by wenzelm
counter added to SAT signature
2005-10-12, by webertj
no proof reconstruction when quick_and_dirty is set
2005-10-12, by webertj
tidying
2005-10-12, by paulson
domain package generates compactness lemmas for new constructors
2005-10-12, by huffman

less more | (0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle