Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
more (co)data docs
2013-10-02, by blanchet
don't register equations of the form 'f x = ...' as simp rules, even if they are safe (noncorecursive), because they unfold too aggresively concepts users are likely to want to stay folded
2013-10-02, by blanchet
NEWS and CONTRIBUTORS
2013-10-02, by traytel
made SML/NJ happy
2013-10-02, by traytel
use new coinduction method and primcorec in examples
2013-10-02, by traytel
new coinduction method
2013-10-02, by traytel
tuned command descriptions
2013-10-02, by blanchet
strengthen tactic w.r.t. let
2013-10-02, by blanchet
minor doc fix (there is no guarantee that the equations for a given f_i are contiguous in the collection)
2013-10-02, by blanchet
typo
2013-10-02, by kuncar
NEWS and CONTRIBUTORS
2013-10-02, by kuncar
merged
2013-10-01, by blanchet
compile -- broken since 21dac9a60f0c
2013-10-01, by blanchet
strengthened tactic for right-hand sides involving lambdas
2013-10-01, by blanchet
basic documentation for function elimination rules and fun_cases
2013-10-01, by krauss
allow uncurried lambda-abstractions on rhs of "primcorec"
2013-10-01, by blanchet
tiny doc fix
2013-10-01, by blanchet
base the fset bnf on the new FSet theory
2013-10-01, by traytel
improved backwards compatiblity of primrec_new (Isabelle/ML interface, attributes, etc.)
2013-10-01, by traytel
removed spurious save if nothing needs to bee learned
2013-10-01, by blanchet
new version of MaSh that really honors the --port option and that checks for file name mismatches
2013-10-01, by blanchet
minor textual changes
2013-10-01, by blanchet
got rid of dead feature
2013-10-01, by blanchet
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
2013-10-01, by blanchet
renamed ML files
2013-10-01, by blanchet
renamed theory file
2013-10-01, by blanchet
tuned signature -- facilitate experimentation with other processes;
2013-10-01, by wenzelm
preserve types during rewriting
2013-09-30, by Christian Sternagel
made SML/NJ happy
2013-09-30, by blanchet
made SML/NJ happy
2013-09-30, by blanchet
made SML/NJ happier
2013-09-30, by blanchet
added experimental configuration options to tune use of builtin symbols in SMT
2013-09-30, by blanchet
added possibility to reset builtins (for experimentation)
2013-09-30, by blanchet
just one data slot (record) per program unit
2013-09-30, by blanchet
more "primrec_new" documentation
2013-09-30, by blanchet
merged
2013-09-30, by wenzelm
tuned signature;
2013-09-30, by wenzelm
eliminated clone of Inductive.mk_cases_tac;
2013-09-30, by wenzelm
tuned signature;
2013-09-30, by wenzelm
tuned whitespace;
2013-09-30, by wenzelm
provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);
2013-09-30, by wenzelm
merge
2013-09-30, by blanchet
minor tweak to error message
2013-09-30, by blanchet
tuned;
2013-09-30, by wenzelm
explicit caret position after replacement;
2013-09-29, by wenzelm
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
generalized case-handling code a bit
2013-09-25, by blanchet
support cases for new-style (co)datatypes
2013-09-25, by blanchet
use case rather than sequence of ifs in expansion
2013-09-25, by blanchet
textual improvements following Christian Sternagel's feedback
2013-09-25, by blanchet
generalize lemma
2013-09-24, by huffman
removed unused lemma
2013-09-24, by huffman
factor out new lemma
2013-09-24, by huffman
replace lemma with more general simp rule
2013-09-24, by huffman
generalized tactics
2013-09-24, by blanchet
renamed generated property
2013-09-24, by blanchet
commented out debugging output in "primcorec"
2013-09-24, by blanchet
merged
2013-09-24, by wenzelm
tuned proofs;
2013-09-24, by wenzelm
more quasi-generic PIDE modules (NB: Swing/JFX needs to be kept separate from non-GUI material);
2013-09-24, by wenzelm
NEWS;
2013-09-24, by wenzelm
clarified font;
2013-09-24, by wenzelm
simplified default L&F -- Nimbus should be always available and GTK+ is not fully working yet;
2013-09-24, by wenzelm
proper platform-specific test;
2013-09-24, by wenzelm
disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
2013-09-24, by wenzelm
focus text field, to capture key events even on Mac OS X look-and-feel;
2013-09-24, by wenzelm
tuned proofs;
2013-09-24, by wenzelm
more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;
2013-09-24, by wenzelm
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
2013-09-24, by wenzelm
clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer);
2013-09-24, by wenzelm
tuned proofs;
2013-09-24, by wenzelm
obsolete;
2013-09-24, by wenzelm
tuned;
2013-09-24, by wenzelm
avoid clash of auto print functions with query operations, notably sledgehammer (cf. 3461985dcbc3);
2013-09-24, by wenzelm
tuned isatest options;
2013-09-24, by wenzelm
updated docs
2013-09-24, by blanchet
added [dest] to "disc_exclude"
2013-09-24, by blanchet
started adding support for "nat_case" as case study for all "case" constructs
2013-09-24, by blanchet
temporary fix to tactic
2013-09-24, by blanchet
made SML/NJ happy
2013-09-24, by blanchet
tuning
2013-09-24, by blanchet
support "of" syntax to disambiguate selector equations
2013-09-24, by panny
don't note more induction principles than there are functions + tuning
2013-09-24, by blanchet
more (co)data docs
2013-09-24, by blanchet
improved rail diagram
2013-09-24, by blanchet
use "primcorec" in example
2013-09-24, by blanchet
use "primcorec" in doc
2013-09-24, by blanchet
updated keywords
2013-09-24, by blanchet
updated certificates
2013-09-24, by blanchet
when "max_thm_instances" is hit, choose more carefully which instances should be kept
2013-09-24, by blanchet
add "primcorec" command (cf. ae7f50e70c09)
2013-09-24, by panny
merged
2013-09-24, by nipkow
added lemmas
2013-09-24, by nipkow
honor MaSh's zero-overhead policy -- no learning if the tool is disabled
2013-09-24, by blanchet
adapted to reflect renaming of session
2013-09-24, by blanchet
merged
2013-09-24, by Andreas Lochbihler
make measure_of total
2013-09-24, by Andreas Lochbihler
encode goal digest in spying log (to detect duplicates)
2013-09-24, by blanchet
made SML/NJ happy
2013-09-24, by blanchet
tuned proofs
2013-09-23, by huffman
use forthcoming "primcorec" command
2013-09-24, by blanchet
set code and nitpick_simp attributes on primcorec theorems
2013-09-24, by blanchet
tuning
2013-09-24, by blanchet
tuned docs
2013-09-24, by blanchet
register codatatypes with Nitpick
2013-09-24, by blanchet
register codatatypes with Nitpick
2013-09-23, by blanchet
don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)
2013-09-23, by blanchet
added [code] to selectors
2013-09-23, by blanchet
tuned spying
2013-09-23, by blanchet
document "spy"
2013-09-23, by blanchet
added "spy" option to Nitpick
2013-09-23, by blanchet
document "spy" option
2013-09-23, by blanchet
added "spy" option to Sledgehammer
2013-09-23, by blanchet
proper text for document preparation;
2013-09-23, by wenzelm
set [code] on case equations
2013-09-23, by blanchet
note coinduct theorems in "primcorec"
2013-09-23, by blanchet
tuning
2013-09-23, by blanchet
generate "simps" from "primcorec"
2013-09-23, by blanchet
undid copy-paste
2013-09-23, by blanchet
avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)
2013-09-23, by blanchet
don't generate empty theorem collections
2013-09-23, by blanchet
less
more
|
(0)
-30000
-10000
-3000
-1000
-240
+240
+1000
+3000
+10000
tip