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 a few lemmas to do with permutation-equivalence for the
2006-02-19, by urbanc
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
2006-02-19, by kleing
use minimal imports
2006-02-19, by huffman
use qualified name for return
2006-02-19, by huffman
dest_def: tuned error msg;
2006-02-18, by wenzelm
const constraints: provide TFrees instead of TVars,
2006-02-17, by wenzelm
checkpoint/copy_node: reset body context;
2006-02-17, by wenzelm
global_qeds: transfer body context;
2006-02-17, by wenzelm
add_const_constraint(_i): demand TFrees instead of TVars, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
constrain: assert const declaration, optional type (i.e. may delete constraints);
2006-02-17, by wenzelm
removed Import/lazy_scan.ML;
2006-02-17, by wenzelm
hyperlinks in the PDF work now
2006-02-17, by paulson
replaced Symbol.explode by explode
2006-02-17, by obua
updated mailing list archive link
2006-02-17, by haftmann
use monomorphic sequences / scanners
2006-02-17, by obua
make maybe into a real type constructor; remove monad syntax
2006-02-17, by huffman
use VectorScannerSeq instead of ListScannerSeq in xml.ML
2006-02-16, by obua
removed lazy_scan
2006-02-16, by obua
improved scanning
2006-02-16, by obua
tuned;
2006-02-16, by wenzelm
Abstract Natural Numbers with polymorphic recursion.
2006-02-16, by wenzelm
new-style definitions/abbreviations;
2006-02-16, by wenzelm
added ex/Abstract_NAT.thy;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
removed silly stuff
2006-02-16, by haftmann
* Isar/locales: new derived specification elements 'definition', 'abbreviation', 'axiomatization';
2006-02-16, by wenzelm
added abbreviation(_i);
2006-02-16, by wenzelm
added put_thms_internal: local_naming, no fact index;
2006-02-16, by wenzelm
added put_thms_internal;
2006-02-16, by wenzelm
added abbrev element;
2006-02-16, by wenzelm
added 'abbreviation';
2006-02-16, by wenzelm
added premsN;
2006-02-16, by wenzelm
Proof.put_thms_internal;
2006-02-16, by wenzelm
removed pointless replace;
2006-02-16, by wenzelm
tuned;
2006-02-16, by wenzelm
dest_def: actually return beta-eta contracted equation;
2006-02-16, by wenzelm
derived specifications: definition, abbreviation, axiomatization;
2006-02-16, by wenzelm
updated;
2006-02-16, by wenzelm
cache improvements
2006-02-16, by obua
variable counter is now also cached
2006-02-16, by obua
adapted to kernel changes
2006-02-16, by obua
tuned subst_bound(s);
2006-02-16, by wenzelm
fixed bugs, added caching
2006-02-15, by obua
added cases_node;
2006-02-15, by wenzelm
replaced qualified_force_prefix to sticky_prefix;
2006-02-15, by wenzelm
removed distinct, renamed gen_distinct to distinct;
2006-02-15, by wenzelm
check_text: Toplevel.node option;
2006-02-15, by wenzelm
init/exit no longer change the theory (no naming);
2006-02-15, by wenzelm
evaluate antiquotes depending on Toplevel.node option;
2006-02-15, by wenzelm
simplified presentation commands;
2006-02-15, by wenzelm
sane version of distinct_subgoals_tac, based on composition with Drule.distinct_prems_rl;
2006-02-15, by wenzelm
removed qualified_force_prefix;
2006-02-15, by wenzelm
replaced qualified_force_prefix to sticky_prefix;
2006-02-15, by wenzelm
chop is no longer pervasive;
2006-02-15, by wenzelm
rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
2006-02-15, by wenzelm
added distinct_prems_rl;
2006-02-15, by wenzelm
specifications_of: avoid partiality;
2006-02-15, by wenzelm
counter example: avoid vacuous trace;
2006-02-15, by wenzelm
cannot use section before setup;
2006-02-15, by wenzelm

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

isabelle