isabelle: Graph

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

tuned proofs
2013-09-29, by haftmann
observe user preferences;
2013-09-29, by wenzelm
updated for release;
2013-09-29, by wenzelm
tuned;
2013-09-29, by wenzelm
tuned;
2013-09-29, by wenzelm
more on text completion;
2013-09-29, by wenzelm
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
2013-09-29, by wenzelm
updated for release;
2013-09-29, by wenzelm
updated for release;
2013-09-29, by wenzelm
updated to sumatra_pdf-2.3.2;
2013-09-29, by wenzelm
low-priority print task is always asynchronous -- relevant for single-core machine and automatically tried tools;
2013-09-29, by wenzelm
backout c6297fa1031a -- strange parsers are required to make this work;
2013-09-29, by wenzelm
make SML/NJ more happy;
2013-09-28, by wenzelm
enforce IsabelleText font for better symbol coverage, especially on Windows;
2013-09-28, by wenzelm
proper wrapper for parser -- more explicit error;
2013-09-28, by wenzelm
misc tuning for release;
2013-09-28, by wenzelm
remove remains from WinRun4J;
2013-09-28, by wenzelm
proper document markup;
2013-09-28, by wenzelm
uniform $ISABELLE_HOME on all platforms;
2013-09-28, by wenzelm
simplified ISABELLE_HOME on Windows (see also 9c8a1b9c0630, 5a7903ba2dac);
2013-09-28, by wenzelm
update second environment that is used for System.getenv(String);
2013-09-28, by wenzelm
adhoc update of JVM environment variables, which is relevant for cold start of jEdit;
2013-09-28, by wenzelm
tuned names
2013-09-27, by kuncar
fold and lemmas about cardinality
2013-09-27, by kuncar
more robust parser: 'imports' are mandatory except for bootstrapping Pure;
2013-09-27, by wenzelm
one more unfolding necessary
2013-09-27, by blanchet
faster exit in common case
2013-09-27, by blanchet
merged
2013-09-27, by nipkow
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
simplified directory structure;
2013-09-25, by wenzelm
obsolete (see da57c4912987);
2013-09-25, by wenzelm
don't generate wrong type
2013-09-25, by blanchet
proper handling of abstractions
2013-09-25, by blanchet
fixed off-by-one bug
2013-09-25, by blanchet
further improved 'code' helper functions
2013-09-25, by blanchet
removed spurious recursion
2013-09-25, by blanchet
robustness
2013-09-25, by blanchet
thread through bound types
2013-09-25, by blanchet
killed redundant argument
2013-09-25, by blanchet
improved massaging of case expressions
2013-09-25, by blanchet
filled in gap in library offering
2013-09-25, by blanchet
updated documentation concerning MacOSX plugin 1.3;
2013-09-25, by wenzelm
merged
2013-09-25, by wenzelm
bypass Isabelle OSX_Adapter for now -- MacOSX plugin 1.3 manages that better;
2013-09-25, by wenzelm
include MacOSX plugin by default -- disabled by default to avoid multiplatform confusion;
2013-09-25, by wenzelm
removed obsolete cobra.jar, js.jar (see also 30de372ca56f);
2013-09-25, by wenzelm
merged
2013-09-25, by nipkow
tuned
2013-09-25, by nipkow
break more conjunctions
2013-09-25, by blanchet
move useful functions to library
2013-09-25, by blanchet
merge
2013-09-25, by panny
simplified code
2013-09-25, by panny
add non-corecursive constructor view theorems to simps
2013-09-25, by panny
merged
2013-09-25, by wenzelm
tuned proofs;
2013-09-25, by wenzelm
explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
2013-09-25, by wenzelm
more powerful fold
2013-09-25, by blanchet
properly fold over branches
2013-09-25, by blanchet
tuned
2013-09-25, by nipkow
removed dead code
2013-09-25, by blanchet
keep a database of free constructor type information
2013-09-25, by blanchet