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

removed obsolete keyword 'files';
2006-01-28, by wenzelm
(un)folded: support object-level rewrites;
2006-01-28, by wenzelm
added equals_cong;
2006-01-28, by wenzelm
added Isar/local_defs.ML;
2006-01-28, by wenzelm
LocalDefs.add_def;
2006-01-28, by wenzelm
LocalDefs.def_export;
2006-01-28, by wenzelm
tuned proofs;
2006-01-28, by wenzelm
Pure/Isar: (un)folded, (un)fold, unfolding support
2006-01-28, by wenzelm
interrupt_timeout for Poly replaced by stub
2006-01-27, by webertj
added atomize_iff;
2006-01-27, by wenzelm
renamed Pretty.gen_list to Pretty.enum;
2006-01-27, by wenzelm
swapped theory_context;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
added invent_fixes;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
renamed reverse_atomize to unatomize;
2006-01-27, by wenzelm
init: include view;
2006-01-27, by wenzelm
improved 'notes', including proper treatment of locale results;
2006-01-27, by wenzelm
swapped Toplevel.theory_context;
2006-01-27, by wenzelm
Locale.init;
2006-01-27, by wenzelm
renamed gen_list to enum;
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
added ProofContext.pprint_context (depends on ProofContext.debug);
2006-01-27, by wenzelm
moved theorem tags from Drule to PureThy;
2006-01-27, by wenzelm
tidying up SPASS output
2006-01-27, by paulson
tidying
2006-01-27, by paulson
better reporting
2006-01-27, by paulson
Interface to access the specification of a named locale.
2006-01-27, by ballarin
Added new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Added in new file Tools/ATP/reduce_axiomsN.ML
2006-01-27, by mengj
Changed codes that call relevance filter.
2006-01-27, by mengj
Relevance filtering. Has replaced the previous version.
2006-01-27, by mengj
interrupt_timeout now raises Interrupt instead of SML90.Interrupt
2006-01-26, by webertj
smaller example to prevent timeout
2006-01-26, by webertj
Fixed bug in code generator for primitive definitions that
2006-01-26, by berghofe
Inductive sets with no introduction rules are now allowed as well.
2006-01-26, by berghofe
added definition(_i);
2006-01-25, by wenzelm
renamed export to export_standard (again!), because it includes Drule.local_standard';
2006-01-25, by wenzelm
ProofContext.export_standard;
2006-01-25, by wenzelm
tuned atomize_cterm;
2006-01-25, by wenzelm
turned abstract_term into ProofContext.abs_def;
2006-01-25, by wenzelm
added constant definition;
2006-01-25, by wenzelm
added 'definition';
2006-01-25, by wenzelm
tuned comment;
2006-01-25, by wenzelm
export name_multi;
2006-01-25, by wenzelm
abs_def: improved error;
2006-01-25, by wenzelm
ObjectLogic.atomize_cterm;
2006-01-25, by wenzelm
updated;
2006-01-25, by wenzelm
works with DPLL solver now
2006-01-24, by webertj
the additional freshness-condition in the one-induction
2006-01-24, by urbanc
fixed code_generate syntax;
2006-01-24, by wenzelm
renamed axiomatize(_i) to axiomatization(_i);
2006-01-24, by wenzelm
renamed inferred_type to inferred_param;
2006-01-24, by wenzelm
ProofContext.inferred_param;
2006-01-24, by wenzelm
removed the_params;
2006-01-24, by wenzelm
added actual operations;
2006-01-24, by wenzelm
axiomatization: optional vars;
2006-01-24, by wenzelm
LocalTheory.pretty_consts;
2006-01-24, by wenzelm
tuned;
2006-01-24, by wenzelm
add_finals: prep_consts, i.e. varify type;
2006-01-24, by wenzelm

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

isabelle