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 context_of -- generic context;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
print rules: generic context;
2006-01-10, by wenzelm
Specification.pretty_consts ctxt;
2006-01-10, by wenzelm
generic data and attributes;
2006-01-10, by wenzelm
added rule, declaration;
2006-01-10, by wenzelm
added generic syntax;
2006-01-10, by wenzelm
tuned dependencies;
2006-01-10, by wenzelm
added declaration_attribute;
2006-01-10, by wenzelm
support for generic contexts with data;
2006-01-10, by wenzelm
fix_tac: no warning;
2006-01-10, by wenzelm
generic attributes;
2006-01-10, by wenzelm
Attrib.rule;
2006-01-10, by wenzelm
tuned
2006-01-10, by urbanc
added the lemmas supp_char and supp_string
2006-01-10, by urbanc
added some lemmas to the collection "abs_fresh"
2006-01-09, by urbanc
_E suffix for compatibility with AddIffs
2006-01-09, by paulson
tidied
2006-01-09, by paulson
simplified the special-case simprules
2006-01-09, by paulson
theorems need names
2006-01-09, by paulson
commented the transitivity and narrowing proof
2006-01-09, by urbanc
Theory specifications --- with type-inference, but no internal polymorphism.
2006-01-07, by wenzelm
added infer_type, declared_type;
2006-01-07, by wenzelm
added param, spec, named_spec;
2006-01-07, by wenzelm
added init;
2006-01-07, by wenzelm
added 'axiomatization';
2006-01-07, by wenzelm
Specification.pretty_consts;
2006-01-07, by wenzelm
gen_names: preserve empty names;
2006-01-07, by wenzelm
added Isar/specification.ML;
2006-01-07, by wenzelm
updated;
2006-01-07, by wenzelm
another change for the new induct-method
2006-01-07, by urbanc
RuleCases.make_nested;
2006-01-07, by wenzelm
support nested cases;
2006-01-07, by wenzelm
support nested cases;
2006-01-07, by wenzelm
RuleCases.make_common;
2006-01-07, by wenzelm
pretty_locale: backquote notes;
2006-01-07, by wenzelm
RuleCases.make_simple;
2006-01-07, by wenzelm
tuned order;
2006-01-07, by wenzelm
added backquote;
2006-01-07, by wenzelm
RuleCases.make_common/nested;
2006-01-07, by wenzelm
* Provers/induct: improved simultaneous goals -- nested cases;
2006-01-07, by wenzelm
added private datatype nprod (copy of prod) to be
2006-01-07, by urbanc
changed PRO_RED proof to conform with the new induction rules
2006-01-07, by urbanc
prep_meta_eq: reuse mk_rews of local simpset;
2006-01-06, by wenzelm
removed obsolete eqrule_HOL_data.ML;
2006-01-06, by wenzelm
removed obsolete eqrule_FOL_data.ML;
2006-01-06, by wenzelm
simplified EqSubst setup;
2006-01-06, by wenzelm
obsolete, reuse mk_rews of local simpset;
2006-01-06, by wenzelm
Toplevel.theory_to_proof;
2006-01-06, by wenzelm
transactions now always see quasi-functional intermediate checkpoint;
2006-01-06, by wenzelm
tuned EqSubst setup;
2006-01-06, by wenzelm
Pure/Isar: Toplevel.theory_to_proof admits transactions that modify the theory;
2006-01-06, by wenzelm
hide type datatype node;
2006-01-05, by wenzelm
tuned print_theorems_theory;
2006-01-05, by wenzelm
Toplevel.proof_position_of;
2006-01-05, by wenzelm
store_thm: transfer to current context, i.e. the target theory;
2006-01-05, by wenzelm
replaced swap by contrapos_np;
2006-01-05, by wenzelm
added setminus;
2006-01-05, by wenzelm
proper handling of simultaneous goals and mutual rules;
2006-01-05, by wenzelm
provide projections of induct_weak, induct_unsafe;
2006-01-05, by wenzelm

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

isabelle