isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 tip

order_tac: prevent potential bug, improve perf and tracing
9 months ago, by Lukas Stevens
misc tuning and clarification;
9 months ago, by wenzelm
clarified antiquotations;
9 months ago, by wenzelm
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
9 months ago, by wenzelm
clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
9 months ago, by wenzelm
avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
9 months ago, by wenzelm
added Thm.instantiate_beta;
9 months ago, by wenzelm
moved generic implementation into HOL-Main
9 months ago, by haftmann
tuned;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified antiquotations;
9 months ago, by wenzelm
clarified antiquotations;
9 months ago, by wenzelm
discontinued somewhat pointless antiquotations;
9 months ago, by wenzelm
NEWS;
9 months ago, by wenzelm
clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
9 months ago, by wenzelm
clarified antiquotations;
9 months ago, by wenzelm
clarified antiquotations;
9 months ago, by wenzelm
clarified antiquotations;
9 months ago, by wenzelm
clarified antiquotations;
9 months ago, by wenzelm
support for "lemma";
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
local fixes for "lemma" antiquotation;
9 months ago, by wenzelm
clarified signature;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified keywords: major take precedence for commands, but not used for antiquotations;
9 months ago, by wenzelm
tuned modules;
9 months ago, by wenzelm
more antiquotations;
9 months ago, by wenzelm
moved a theorem to a sensible place
9 months ago, by paulson
merged
9 months ago, by wenzelm
tuned, continuing e955964d89cb;
9 months ago, by wenzelm
avoid waste of resources due to dynamic simpset (amending 45c09620f726);
9 months ago, by wenzelm
fix latex
9 months ago, by Norbert Schirmer
clarified modules;
9 months ago, by wenzelm
more generic bit/word lemmas for distribution
9 months ago, by haftmann
merged
9 months ago, by paulson
Added / moved some simple set-theoretic lemmas
9 months ago, by paulson
more CONTRIBUTORS and NEWS;
9 months ago, by wenzelm
cleanup; add Apple reference
9 months ago, by Norbert Schirmer
refine interface
13 months ago, by Norbert Schirmer
generalized component lookup for syntax and distinctness proofs. added some tracing.
21 months ago, by Norbert Schirmer
merged
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
more antiquotations;
9 months ago, by wenzelm
more antiquotations;
9 months ago, by wenzelm
more robust: genuinely free variables need to be instantiated;
9 months ago, by wenzelm
tuned comments;
9 months ago, by wenzelm
clarified errors;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
9 months ago, by wenzelm
tuned;
9 months ago, by wenzelm
clarified signature -- avoid clones;
9 months ago, by wenzelm
Refinement of partitions
9 months ago, by paulson
avoid persistence of static context: instantiation arguments should provide proper dynamic context;
9 months ago, by wenzelm
more antiquotations;
9 months ago, by wenzelm
more markup;
9 months ago, by wenzelm
clarified name, syntax, messages;
9 months ago, by wenzelm
more antiquotations;
9 months ago, by wenzelm
more control symbols;
9 months ago, by wenzelm
tuned signature;
9 months ago, by wenzelm
ML antiquotations to instantiate types/terms/props;
9 months ago, by wenzelm

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

isabelle