isabelle: Graph

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
tuned code
2013-09-23, by blanchet
provide a way to override MaSh's port from configuration file
2013-09-23, by blanchet
new version of MaSh program, with proper shutdown
2013-09-23, by blanchet
tuned proofs;
2013-09-22, by wenzelm
focus on default component according to jEdit window management;
2013-09-22, by wenzelm
tuned;
2013-09-22, by wenzelm
tuned signature;
2013-09-22, by wenzelm
completion popup for history text field;
2013-09-22, by wenzelm
clarified location of GUI modules (which depend on Swing of JFX);
2013-09-22, by wenzelm
repaired latex (cf. 7bb0cf27c243);
2013-09-21, by wenzelm
tuned proofs;
2013-09-21, by wenzelm
caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view);
2013-09-21, by wenzelm
tuned;
2013-09-21, by wenzelm
proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);
2013-09-21, by wenzelm
immediate access to some elementary examples;
2013-09-21, by wenzelm
more front-matter;
2013-09-21, by wenzelm
clarified logo;
2013-09-21, by wenzelm
proper text replacement (cf. 747835eb2782);
2013-09-21, by wenzelm
added canonical screenshot;
2013-09-21, by wenzelm
removed obsolete README;
2013-09-21, by wenzelm
tuned;
2013-09-21, by wenzelm
added/updated material from src/Tools/jEdit/README.html;
2013-09-21, by wenzelm
basic setup for Isabelle/jEdit documentation;
2013-09-21, by wenzelm
updated keywords;
2013-09-21, by wenzelm
updated CONTRIBUTORS
2013-09-20, by blanchet
updated NEWS
2013-09-20, by blanchet
document option
2013-09-20, by blanchet
merged "isar_try0" and "isar_minimize" options
2013-09-20, by blanchet
hardcoded obscure option
2013-09-20, by blanchet
hard-coded an obscure option
2013-09-20, by blanchet
use configuration mechanism for low-level tracing
2013-09-20, by blanchet
moved focus to Isabell/jEdit and away from Proof General
2013-09-20, by blanchet
took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired
2013-09-20, by blanchet
tuning (use a blacklist instead of a whitelist)
2013-09-20, by blanchet
reduce the number of emitted MaSh commands (among others to facilitate debugging)
2013-09-20, by blanchet
MaSh tweaks to facilitate debugging
2013-09-20, by blanchet
tuned proofs
2013-09-20, by haftmann
make SML/NJ happy
2013-09-20, by kuncar
renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")
2013-09-20, by blanchet
more primcorec docs
2013-09-20, by blanchet
added primcorec examples with lambdas
2013-09-20, by blanchet
more primcorec docs
2013-09-20, by blanchet
adapted primcorec documentation to reflect the three views
2013-09-20, by blanchet
updated docs
2013-09-20, by blanchet
took out spurious attributes (no need for several code equations / simps for thesame constants)
2013-09-20, by blanchet
have "datatype_new_compat" register induction and recursion theorems in nested case
2013-09-20, by blanchet
prefer Code.abort over code_abort
2013-09-20, by Andreas Lochbihler
setting the stage for safe constructor simp rules
2013-09-20, by blanchet
added TODO
2013-09-19, by blanchet
made tactic more reliable
2013-09-19, by blanchet
killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'
2013-09-19, by blanchet
cleaner handling of collapse theorems
2013-09-19, by blanchet
repaired latex (cf. 84522727f9d3);
2013-09-19, by wenzelm
updated NEWS
2013-09-19, by blanchet
dropped dead code
2013-09-19, by haftmann
don't declare ctr view primcorec theorems as simp (they loop)
2013-09-19, by traytel
simplified code; eliminated some dummyTs
2013-09-19, by panny
avoid infinite loop for unapplied terms + tuning
2013-09-19, by blanchet
generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"
2013-09-19, by blanchet
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"
2013-09-19, by blanchet
added auxiliary function
2013-09-19, by blanchet
avoid parameter
2013-09-19, by blanchet
added helper function for code equations in primcorec
2013-09-19, by blanchet
updated NEWS and CONTRIBUTORS
2013-09-19, by blanchet
split functionality into two functions to avoid redoing work over and over
2013-09-19, by blanchet
added massaging function for primcorec code equations
2013-09-19, by blanchet
simplified code
2013-09-19, by blanchet
no need for beta-eta contraction
2013-09-19, by blanchet
generalize helper function
2013-09-19, by blanchet
generate more theorems (e.g. for types with only one constructor)
2013-09-19, by panny
added two functions to List (one contributed by Manuel Eberl)
2013-09-18, by traytel
generate constructor view theorems
2013-09-18, by panny
merged;
2013-09-18, by wenzelm
merged;
2013-09-18, by wenzelm
tuned proofs;
2013-09-18, by wenzelm
tuned proofs;
2013-09-18, by wenzelm
added option "jedit_auto_load";
2013-09-18, by wenzelm
limit for text height;
2013-09-18, by wenzelm
improved layout, with special treatment for ScrollPane;
2013-09-18, by wenzelm
tuned signature;
2013-09-18, by wenzelm
improved FlowLayout for wrapping of components over multiple lines;
2013-09-18, by wenzelm
updated to polyml-5.5.1;
2013-09-18, by wenzelm
improved printing of exception trace in Poly/ML 5.5.1;
2013-09-18, by wenzelm
more antiquotations;
2013-09-18, by wenzelm
moved module into plain Isabelle/ML user space;
2013-09-18, by wenzelm
more primcorec tactics
2013-09-18, by blanchet
enrich data structure
2013-09-18, by blanchet
include more "discI" rules
2013-09-18, by blanchet
updated docs
2013-09-18, by blanchet
tuning (alphabetical order)
2013-09-18, by blanchet
removed spurious "simp"
2013-09-18, by blanchet
note "discI"
2013-09-18, by blanchet
tuned tactics
2013-09-18, by blanchet
no need thanks to "Code.abort"
2013-09-18, by blanchet
minor change related to code equations in primcorec
2013-09-18, by blanchet
don't unfold as eager as in 11a77e4aa98b
2013-09-18, by traytel
tuned proofs
2013-09-18, by traytel
use singular to avoid confusion
2013-09-18, by blanchet
new tactics for constructor view
2013-09-18, by blanchet
tuning
2013-09-18, by blanchet
fixed embarrassing typo in example
2013-09-18, by blanchet
avoid duplicate simp rule warnings
2013-09-18, by blanchet
added and tuned lemmas
2013-09-18, by nipkow
tuned proofs;
2013-09-18, by wenzelm
updated to official polyml-5.5.1;
2013-09-17, by wenzelm
updated to polyml-5.5.1;
2013-09-17, by wenzelm
actually use x86_64 machine;
2013-09-17, by wenzelm
correct merging of restore data
2013-09-17, by kuncar
order_bot, order_top
2013-09-17, by lammich
include Int_Pow into Quotient_Examples; add end of the theory
2013-09-17, by kuncar
NEWS: Simps_Case_Conv
2013-09-17, by noschinl
added lemmas and made concerse executable
2013-09-17, by nipkow
merge
2013-09-17, by blanchet
return right theorems
2013-09-17, by blanchet
more (co)data docs
2013-09-17, by blanchet
tuned proofs about 'convex'
2013-09-13, by huffman
more (co)data docs
2013-09-17, by blanchet
tuned proofs;
2013-09-17, by wenzelm
treat all dummy type variables separately (in contrast to fca432074fb2);
2013-09-16, by wenzelm