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

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
added strict_mutual_rule;
2006-01-05, by wenzelm
RuleCases.strict_mutual_rule;
2006-01-05, by wenzelm
changed the name of the type "nOption" to "noption".
2006-01-05, by urbanc
added "fresh_singleton" lemma
2006-01-04, by urbanc
added more documentation; will now try out a modification
2006-01-04, by urbanc
Reversed Larry's option/iff change.
2006-01-04, by nipkow
substantial additions using locales
2006-01-04, by haftmann
exported read|cert_arity interfaces
2006-01-04, by haftmann
trace_simp_depth_limit is 1 by default
2006-01-04, by nipkow
removed pointless trace msg.
2006-01-04, by nipkow
preservation of names
2006-01-04, by paulson
a few more named lemmas
2006-01-04, by paulson
fix: reintroduced pred_ctxt in gen_add_locale
2006-01-04, by haftmann
tuned;
2006-01-04, by wenzelm
* Pure/Isar: Toplevel.theory_theory_to_proof;
2006-01-04, by wenzelm
added unlocalize_mfix;
2006-01-04, by wenzelm
added unlocalize_mixfix;
2006-01-04, by wenzelm
added theory_to_theory_to_proof, which may change theory before entering the proof;
2006-01-04, by wenzelm
tuned;
2006-01-04, by wenzelm
moved forget_proof to toplevel.ML;
2006-01-04, by wenzelm
Toplevel.forget_proof;
2006-01-04, by wenzelm
adapted Toplevel.Proof;
2006-01-04, by wenzelm
removed dead code;
2006-01-04, by wenzelm
more stuff;
2006-01-04, by wenzelm
Provers/classical: stricter checks to ensure that supplied intro, dest and
2006-01-03, by paulson
added explicit paths to required theories
2006-01-03, by paulson
added implementation manual;
2006-01-03, by wenzelm
more stuff;
2006-01-03, by wenzelm
fixed LaTeX source;
2006-01-03, by wenzelm
class now a keyword
2006-01-03, by haftmann
class now an keyword, quoted where necessary
2006-01-03, by haftmann
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
2006-01-03, by haftmann
rearranged burrow_split to fold_burrow to allow composition with fold_map
2006-01-03, by haftmann
added unfolding(_i);
2006-01-03, by wenzelm
unparse String/AltString: escape quotes;
2006-01-03, by wenzelm
tuned;
2006-01-03, by wenzelm
avoid hardwired Trueprop;
2006-01-03, by wenzelm
added 'using' command;
2006-01-03, by wenzelm
updated;
2006-01-03, by wenzelm
added IsarImplementation;
2006-01-03, by wenzelm
updated -- lost update!?
2006-01-03, by wenzelm
* Pure/Isar: new command 'unfolding';
2006-01-03, by wenzelm
ISABELLE_USER for remote cvs access;
2006-01-02, by wenzelm
outline;
2006-01-02, by wenzelm
"The Isabelle/Isar Implementation" manual;
2006-01-02, by wenzelm
* Provers/classical: removed obsolete classical version of elim_format;
2005-12-31, by wenzelm
tuned forall_intr_vars;
2005-12-31, by wenzelm
added classical_rule, which replaces Data.make_elim;
2005-12-31, by wenzelm
explicitly reject consts *Goal*, *False*;
2005-12-31, by wenzelm
elim rules: Classical.classical_rule;
2005-12-31, by wenzelm
removed obsolete cla_dist_concl;
2005-12-31, by wenzelm
removed classical elim_format;
2005-12-31, by wenzelm
removed obsolete Provers/make_elim.ML;
2005-12-31, by wenzelm
obsolete, see classical_rule in Provers/classical.ML;
2005-12-31, by wenzelm

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

isabelle