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

discontinued support for 4.1.1, 4.1.2;
2007-10-20, by wenzelm
moved internalM to PrintMode.internal;
2007-10-20, by wenzelm
tuned abbrev interface;
2007-10-20, by wenzelm
tuned abbrev interface;
2007-10-20, by wenzelm
added fixed_abbrev;
2007-10-20, by wenzelm
added input/internal, which are never active in print_mode_value;
2007-10-20, by wenzelm
no_variables: tuned error msg;
2007-10-20, by wenzelm
PrintMode.internal;
2007-10-20, by wenzelm
tuned;
2007-10-20, by wenzelm
add_inductive: more careful handling of abbrevs -- do not expand prematurely;
2007-10-20, by wenzelm
fixed proof: neq0_conv;
2007-10-20, by wenzelm
fixed proofs
2007-10-20, by chaieb
neq0_conv removed from [iff] -- causes problems by simple goals with blast, auto etc...
2007-10-20, by chaieb
export_code: proper command;
2007-10-19, by wenzelm
warn_open: context position;
2007-10-19, by wenzelm
sorry: proper command;
2007-10-19, by wenzelm
tuned proofs: avoid implicit prems;
2007-10-19, by wenzelm
tuned proofs;
2007-10-19, by wenzelm
internal tuning: class_target, fork_mixfix, declare_const (singleton), abbrev;
2007-10-19, by wenzelm
tuned interfaces;
2007-10-19, by wenzelm
tuned
2007-10-19, by haftmann
antisymmetry not a default intro rule any longer
2007-10-19, by haftmann
now employing dictionaries
2007-10-19, by haftmann
added examples
2007-10-19, by haftmann
lemmas with normalization
2007-10-19, by haftmann
tuned CRITICAL markups;
2007-10-19, by wenzelm
do not export standard_infer_types;
2007-10-19, by wenzelm
clarified abbreviations in class context
2007-10-19, by haftmann
Interpretation equations may have name and/or attribute;
2007-10-19, by ballarin
Interpretation equations may have name and/or attribute.
2007-10-19, by ballarin
updated
2007-10-19, by krauss
removed funny formatting
2007-10-19, by krauss
Updated function tutorial: Types can be inferred and need not be given anymore
2007-10-19, by krauss
98% localized
2007-10-19, by haftmann
dropped doubled proof
2007-10-19, by haftmann
Simultaneous type inference using read_specification
2007-10-18, by krauss
some more metis calls
2007-10-18, by paulson
Improving the propagation of type constraints for Frees
2007-10-18, by paulson
Ensured that the right number of ATP calls is generated
2007-10-18, by paulson
CRITICAL evaluation
2007-10-18, by haftmann
improved class syntax
2007-10-18, by haftmann
tuned
2007-10-18, by haftmann
DeclareRobustCommand \isactrlbsub/esub etc.;
2007-10-18, by wenzelm
evaluation is CRITICAL
2007-10-18, by haftmann
moved fork_mixfix to theory_target
2007-10-18, by haftmann
moved lemmas to OrderedGroup.thy
2007-10-18, by haftmann
continued localization
2007-10-18, by haftmann
localized mono predicate
2007-10-18, by haftmann
removed obsolete unlocalize_mfix;
2007-10-17, by wenzelm
removed obsolete unlocalize_mixfix;
2007-10-17, by wenzelm
locale pred: authentic syntax, tuned aprop_tr' accordingly;
2007-10-17, by wenzelm
store external accesses within name space (as produced by naming policy);
2007-10-17, by wenzelm
removed unused set_policy;
2007-10-17, by wenzelm
replaced NameSpace.accesses' by NameSpace.external_names (depening on naming);
2007-10-17, by wenzelm
added sorted_list_of_set
2007-10-17, by nipkow
tuned fork_mixfix (back from class.ML);
2007-10-17, by wenzelm
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
2007-10-17, by wenzelm
removed obsolete fork_mixfix (back to theory_target.ML);
2007-10-17, by wenzelm
updated;
2007-10-17, by wenzelm
clarified fork_mixfix
2007-10-16, by haftmann

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

isabelle