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 +3000 +10000 tip

hide coercion
2013-09-27, by nipkow
fixed one line that would never have compiled in a typed language + release the lock in case of exceptions
2013-09-27, by blanchet
merged
2013-09-27, by nipkow
added Bleast code eqns for RBT
2013-09-27, by nipkow
added code eqns for bounded LEAST operator
2013-09-27, by nipkow
new theory of finite sets as a subtype
2013-09-27, by kuncar
new parametricity rules and useful lemmas
2013-09-27, by kuncar
allow to specify multiple parametricity transfer rules in lift_definition
2013-09-27, by kuncar
merged
2013-09-27, by Andreas Lochbihler
generalise lemma
2013-09-27, by Andreas Lochbihler
proper latex;
2013-09-27, by wenzelm
merged
2013-09-27, by Andreas Lochbihler
add relator for 'a filter and parametricity theorems
2013-09-27, by Andreas Lochbihler
tuned proofs
2013-09-27, by Andreas Lochbihler
add lemmas
2013-09-27, by Andreas Lochbihler
prefer Code.abort over code_abort
2013-09-27, by Andreas Lochbihler
merged
2013-09-27, by lammich
Added Item_Net.retrieve_matching
2013-09-26, by lammich
Added symmetric code_unfold-lemmas for null and is_none
2013-09-26, by lammich
tuned proofs
2013-09-26, by huffman
moved lemma
2013-09-26, by huffman
merged
2013-09-26, by wenzelm
proper regexp;
2013-09-26, by wenzelm
added Isabelle/ML example;
2013-09-26, by wenzelm
updated jedit.jar, jEdit-patched.tar.gz according to 239f8f451976;
2013-09-26, by wenzelm
workaround for action-bar shortcut on Mac OS X L&F: avoid EnhancedMenuItem.setAccelerator which causes conflict with regular key handling and thus double invocation -- see also jEdit.actionContext (if actionBarVisible view.removeToolBar);
2013-09-26, by wenzelm
more uniform modes (NB: comments etc. are handled by isabelle.Token_Markup.Marker);
2013-09-26, by wenzelm
support more brackets (see also 427724cff970, 7bf637b65ba2);
2013-09-26, by wenzelm
tuned proofs
2013-09-26, by huffman
further strengthening of tactics
2013-09-26, by blanchet
merged
2013-09-26, by Andreas Lochbihler
add lemmas
2013-09-26, by Andreas Lochbihler
strengthened tactic
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
avoid calls to nth with ~1
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
strengthened tactic
2013-09-26, by blanchet
tactic cleanup
2013-09-26, by blanchet
made tactic more robust in case somebody specified a discriminator for a one-constructor type
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity
2013-09-26, by blanchet
generate "sel_splits(_asm)" theorems
2013-09-26, by blanchet
generate "sel_exhaust" theorem
2013-09-26, by blanchet
merged
2013-09-26, by wenzelm
obsolete (see also 48d13465c7c7);
2013-09-26, by wenzelm
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
2013-09-26, by wenzelm
initialize class immediately (potentially more robust);
2013-09-26, by wenzelm
tuned
2013-09-26, by nipkow
strengthen tactic
2013-09-26, by blanchet
use needed case theorems
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
added data query function
2013-09-26, by blanchet
added data query function
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
got rid of dependency on silly 'eq_ifI' theorem
2013-09-26, by blanchet
more powerful/robust tactics
2013-09-26, by blanchet
use standard "split" properties instead of ad hoc "eq_...I"
2013-09-26, by blanchet
tuning
2013-09-26, by blanchet
made tactic more flexible w.r.t. case expressions and such
2013-09-26, by blanchet
simplified code
2013-09-25, by panny

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

isabelle