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

Adapted to new type of PureThy.add_defs_i.
2005-12-08, by berghofe
replaced swap by Classical.swap;
2005-12-07, by wenzelm
avoid unportable tail;
2005-12-07, by wenzelm
tuned
2005-12-07, by urbanc
removed thms 'swap' and 'nth_map' from ML toplevel
2005-12-06, by haftmann
improved serialization of classes to haskell
2005-12-06, by haftmann
improved class handling
2005-12-06, by haftmann
added 'dig' combinator
2005-12-06, by haftmann
re-oriented some result tuples in PureThy
2005-12-06, by haftmann
Added more functions for new type embedding of HOL clauses.
2005-12-06, by mengj
Added new type embedding methods for translating HOL clauses.
2005-12-06, by mengj
added code to say that discrete types (nat, bool, char)
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
transitivity should be now in a reasonable state. But
2005-12-05, by urbanc
tuned
2005-12-05, by urbanc
ISAR-fied two proofs
2005-12-05, by urbanc
Adapted to new type of store_thmss(_atts).
2005-12-05, by berghofe
Added store_thmss_atts to signature again.
2005-12-05, by berghofe
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
tuned
2005-12-04, by urbanc
added an Isar-proof for the abs_ALL lemma
2005-12-04, by urbanc
tuning
2005-12-04, by urbanc
defines: beta/eta contract lhs;
2005-12-02, by wenzelm
asts_to_terms: builtin free_fixed translation makes local binders work properly;
2005-12-02, by wenzelm
mixfix_args: 1 for binders;
2005-12-02, by wenzelm
removed fixed_tr: now handled in syntax module;
2005-12-02, by wenzelm
added mixfixT;
2005-12-02, by wenzelm
defs: beta/eta contract lhs;
2005-12-02, by wenzelm
abs_def: beta/eta contract lhs;
2005-12-02, by wenzelm
Added recdef congruence rules for bounded quantifiers and commonly used
2005-12-02, by krauss
various improvements
2005-12-02, by haftmann
adjusted to improved code generator interface
2005-12-02, by haftmann
added perhaps option combinator
2005-12-02, by haftmann
adopted keyword for code generator
2005-12-02, by haftmann
Factored out proof for normalization of applications (norm_list).
2005-12-02, by berghofe
introduced new map2, fold
2005-12-02, by haftmann
typo
2005-12-01, by kleing
simprocs: static evaluation of simpset;
2005-12-01, by wenzelm
tuned;
2005-12-01, by wenzelm
tuned msg;
2005-12-01, by wenzelm
ProofContext.lthms_containing: suppress obvious duplicates;
2005-12-01, by wenzelm
unfold_tac: static evaluation of simpset;
2005-12-01, by wenzelm
superceded by timestart|stop.bash;
2005-12-01, by wenzelm
cpu time = user + system;
2005-12-01, by wenzelm
replaced lib/scripts/showtime by more advanced lib/scripts/timestart|stop.bash;
2005-12-01, by wenzelm
assoc_consts and assoc_types now check number of arguments in template.
2005-12-01, by berghofe
Added new component "sorts" to record datatype_info.
2005-12-01, by berghofe
timestop - report timing based on environment (cf. timestart.bash);
2005-12-01, by wenzelm
timestart - setup bash environment for timing;
2005-12-01, by wenzelm
Improved norm_proof to handle proofs containing term (type) variables
2005-12-01, by berghofe
restoring the old status of subset_refl
2005-12-01, by paulson
oriented pairs theory * 'a to 'a * theory
2005-12-01, by haftmann
initial cleanup to use the new induction method
2005-12-01, by urbanc
cleaned up further the proofs (diamond still needs work);
2005-12-01, by urbanc
changed "fresh:" to "avoiding:" and cleaned up the weakening example
2005-12-01, by urbanc
match_bind(_i): return terms;
2005-11-30, by wenzelm
method 'fact': SIMPLE_METHOD, i.e. insert facts;
2005-11-30, by wenzelm
simulaneous 'def';
2005-11-30, by wenzelm
added facilities to prove the pt and fs instances
2005-11-30, by urbanc

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

isabelle