don't note more induction principles than there are functions + tuning

more (co)data docs

improved rail diagram

use "primcorec" in example

use "primcorec" in doc

updated keywords

updated certificates

when "max_thm_instances" is hit, choose more carefully which instances should be kept

add "primcorec" command (cf. ae7f50e70c09)

merged

added lemmas

honor MaSh's zero-overhead policy -- no learning if the tool is disabled

adapted to reflect renaming of session

merged

make measure_of total

encode goal digest in spying log (to detect duplicates)

made SML/NJ happy

tuned proofs

use forthcoming "primcorec" command

set code and nitpick_simp attributes on primcorec theorems

tuning

tuned docs

register codatatypes with Nitpick

register codatatypes with Nitpick

don't generalize w.r.t. wrong context -- better overgeneralize (since the instantiation phase will compensate for it)

added [code] to selectors

tuned spying

document "spy"

added "spy" option to Nitpick

document "spy" option

added "spy" option to Sledgehammer

proper text for document preparation;

set [code] on case equations

note coinduct theorems in "primcorec"

tuning

generate "simps" from "primcorec"

undid copy-paste

avoid giving same name to simplifying constructor as to real one (to avoid risks of confusion when reading the code)

don't generate empty theorem collections

tuned code

provide a way to override MaSh's port from configuration file

new version of MaSh program, with proper shutdown

tuned proofs;

focus on default component according to jEdit window management;

tuned;

tuned signature;

completion popup for history text field; imitate view font, for default rendering of symbols; tuned signature;

clarified location of GUI modules (which depend on Swing of JFX);

repaired latex (cf. 7bb0cf27c243);

tuned proofs;

caret range of active text area counts as visible (e.g. relevant for Output after scrolling outside of text view);

tuned;

proper layered pane at root of parent component, not global view (e.g. relevant for tooltips for detached info windows);

immediate access to some elementary examples;

more front-matter;

clarified logo;

proper text replacement (cf. 747835eb2782);

added canonical screenshot;

removed obsolete README; open Documentation dockable by default;

tuned;

added/updated material from src/Tools/jEdit/README.html;

basic setup for Isabelle/jEdit documentation;

updated keywords;

updated CONTRIBUTORS

updated NEWS

document option

merged "isar_try0" and "isar_minimize" options

hardcoded obscure option

hard-coded an obscure option

use configuration mechanism for low-level tracing

moved focus to Isabell/jEdit and away from Proof General

took out Waldmeister from list of default provers -- it's usually just visual noise, and its integration in Sledgehammer leaves much to be desired

tuning (use a blacklist instead of a whitelist)

reduce the number of emitted MaSh commands (among others to facilitate debugging)

MaSh tweaks to facilitate debugging

tuned proofs

make SML/NJ happy

renamed "primcorec" to "primcorecursive", to open the door to a 'theory -> theory' command called "primcorec" (cf. "fun" vs. "function")

more primcorec docs

added primcorec examples with lambdas

more primcorec docs

adapted primcorec documentation to reflect the three views

updated docs

took out spurious attributes (no need for several code equations / simps for thesame constants)

have "datatype_new_compat" register induction and recursion theorems in nested case

prefer Code.abort over code_abort

setting the stage for safe constructor simp rules

added TODO

made tactic more reliable

killed exceptional code that is anyway no longer needed, now that the 'simp' attribute has been taken away -- this solves issues in 'primcorec'

cleaner handling of collapse theorems

repaired latex (cf. 84522727f9d3);

updated NEWS

dropped dead code

don't declare ctr view primcorec theorems as simp (they loop)

simplified code; eliminated some dummyTs

avoid infinite loop for unapplied terms + tuning

generalize code to handle zero-argument case gracefully (e.g. for nullay functions defined over codatatypes that corecurse through "fun"

give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"

added auxiliary function

avoid parameter

added helper function for code equations in primcorec

updated NEWS and CONTRIBUTORS

split functionality into two functions to avoid redoing work over and over

added massaging function for primcorec code equations

simplified code

no need for beta-eta contraction

generalize helper function

generate more theorems (e.g. for types with only one constructor)

added two functions to List (one contributed by Manuel Eberl)

generate constructor view theorems

merged;

merged;

tuned proofs;

tuned proofs;

added option "jedit_auto_load"; allow in-place change of option "editor_continuous_checking";

limit for text height;

improved layout, with special treatment for ScrollPane;

tuned signature;

improved FlowLayout for wrapping of components over multiple lines;

updated to polyml-5.5.1;

improved printing of exception trace in Poly/ML 5.5.1;

more antiquotations; tuned signature;

moved module into plain Isabelle/ML user space;

more primcorec tactics

enrich data structure

include more "discI" rules

updated docs

tuning (alphabetical order)

removed spurious "simp"

note "discI"

tuned tactics

no need thanks to "Code.abort"

minor change related to code equations in primcorec

don't unfold as eager as in 11a77e4aa98b

tuned proofs

use singular to avoid confusion

new tactics for constructor view

tuning

fixed embarrassing typo in example

avoid duplicate simp rule warnings

added and tuned lemmas

tuned proofs;

updated to official polyml-5.5.1;

updated to polyml-5.5.1; prefer explicit POLYML_HOME to simplify additional user settings;

actually use x86_64 machine;

correct merging of restore data

order_bot, order_top

include Int_Pow into Quotient_Examples; add end of the theory

NEWS: Simps_Case_Conv

added lemmas and made concerse executable

merge

return right theorems

more (co)data docs

tuned proofs about 'convex'

more (co)data docs

tuned proofs;

treat all dummy type variables separately (in contrast to fca432074fb2);

removed dead code (see also 69d4543811d0);

merged

tuned signature;

more antiquotations -- avoid unchecked string literals;

more explicit exception pattern (NB: unqualified exceptions without arguments are in danger of becoming catch-all patterns by accident);

distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions; some notes about missing ML interface;

tuned white space; avoid "object-oriented English";

adhoc check of ML sources, in addition to thy files already covered in Thy_Load;

proper Isabelle symbols -- no UTF8 here;

proper Cygwin mirror for Isabelle2013-1;

explicit test of quick_and_dirty, which is rarely used in practice;

updated to cygwin-20130916;

more CHECKLIST;

updated cygwin snapshot;

updated to smlnj 110.76;

prefer high-level ML_System.share_common_data, ML_System.save_state -- except for bootstrap images (RAW, Pure);

more NEWS;

merge

prove simp theorems for newly generated definitions

example using restoring Transfer/Lifting context

use lifting_forget for deregistering numeric types as a quotient type

restoring Transfer/Lifting context

make ML function for deleting quotients public

public access to the raw transfer rules - for restoring transferring

another move to avoid sporadic kill of poly, which is presumably due to resource management on lxbroy2, lxbroy3 etc.;

more (co)data docs

more (co)data docs

added missing theorems to "simps" collection

more (co)data docs

more (co)data docs

more (co)data docs

merged

tuned proofs;

tuned magic number, for improved reactivity on old 2-core machine;