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

added attributes defn_add/del;
2006-01-29, by wenzelm
added 'defn' attribute;
2006-01-29, by wenzelm
proper order of trfuns;
2006-01-29, by wenzelm
CPure: Context.add_setup;
2006-01-29, by wenzelm
tuned proofs;
2006-01-29, by wenzelm
implicit setup;
2006-01-29, by wenzelm
default rule step: norm_hhf_tac;
2006-01-29, by wenzelm
tuned comment;
2006-01-29, by wenzelm
declare 'defn' rules;
2006-01-29, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
Basic operations on local definitions.
2006-01-28, by wenzelm
removed unnecessary Syntax.fix_mixfix;
2006-01-28, by wenzelm
added axiomatization_loc, definition_loc;
2006-01-28, by wenzelm
moved local defs to local_defs.ML;
2006-01-28, by wenzelm
LocalDefs;
2006-01-28, by wenzelm
removed unatomize;
2006-01-28, by wenzelm
(un)fold: support object-level rewrites;
2006-01-28, by wenzelm
added print_consts;
2006-01-28, by wenzelm
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

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

isabelle