by default, only generate one discriminator for a two-value datatype

eliminated potentially confusing terminology of Scala "layer";

merged

tuned proofs;

discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;

honor mixfix specifications

code indentation

print timing information

adapted example

check type variables on rhs

proper subsexp projection of Isabelle_Markup.Path, in correspondence to 5d0cd770828e;

added tooltip to reveal jEdit platform file name;

commented out slow examples again

fixed (n + 1)st bug in "mk_exhaust_tac" -- arose with uncurried constructors

fixed "mk_exhaust_tac" for the nth time

updated README

ported "Misc_Codata" to new syntax

ported "Misc_Data" to new syntax

error message only in case of an error

do not trivialize important internal theorem in quick_and_dirty mode

merged

made "mk_case_eq_tac" work in the case where the first constructor is an "alternate" constructor (in which case its discriminator paradoxically starts with a negation)

tuning (systematic 1-based indices)

reindented code

added TODO

tell "select_prem_tac" not to thin any further premisses -- the "rotate_tac" otherwise confuses it

fixed "mk_alternate_disc_def_tac" in the case where the constructors are swapped compared with the common Nil/Cons case

don't get confused by extraneous premisses

added a check

NEWS; CONTRIBUTORS

misc tuning;

no need to wait 3h on macbroy30 (unlike former macbroy6, cf. 6e5b994070c1);

more conservative rechecking of processed constraints in subtyping constraint simplification

added comment for Dmitriy

fixed bug in type instantiation of case theorem

use empty binding rather than "*" for default

tuned

fixed bugs in one-constructor case

smoothly handle one-constructor types

fixed some type issues in sugar "exhaust_tac"

optionally provide extra dead variables to the FP constructions

merged

added robustness

added build option -R; more precise build_doc, using build -R -b;

implemented "mk_case_tac" -- and got rid of "cheat_tac"

define "case" constant

renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix

implemented "mk_half_distinct_tac"

implemented "mk_inject_tac"

implemented "mk_exhaust_tac"

more work on FP sugar

more work on sugar + simplify Trueprop + eq idiom everywhere

renamed "disc_exclus" theorem to "disc_exclude"

more work on FP sugar

smarter "*" syntax -- fallback on "_" if "*" is impossible

more work on FP sugar

renamed theorem

tuned TODO comment

allow pseudo-definition of is_Cons in terms of is_Nil (and similarly for other two-constructor datatypes)

removed oddities

allow "*" to indicate no discriminator

tuned TODOs

started work on sugared "(co)data" commands

export "wrap" function

eliminated obsolete "parallel_proofs = 0" restriction (cf. 0e5b859e1c91)

no more aliases for Local_Theory.note; use Thm.close_derivation in internal theorems;

enable parallel terminal proofs in interaction;

misc tuning;

merged

killed internal output

generate coinductive witnesses for codatatypes

generalized signature

added examples for testing of coinductive witnesses

continue with more robust dummy session after failed startup;

prefer old startup dialog scheme (cf. 514bb82514df);

more permissive handling of plugin startup failure;

bypass slow check for inlined files, where it is not really required;

more direct access to all-important chunks for text painting; clarified line_start offset: physical line start not start(i);

merged

added annotations after condition in if and while

merge, resolving trivial conflict;

forgot to add lemmas

hide newly introduced constant Sublist.sub to allow for name sub in TreeFsetI

reverted (accidentally commited) changes from changeset fd4aef9bc7a9

reverted (accidentally commited) changes from changeset fd4aef9bc7a9

added theory instantiating type class order for list prefixes

Main is implicitly imported via Sublist

added author

List is implicitly imported by Main

introduced "sub" as abbreviation for "emb (op =)"; Sublist_Order is now based on Sublist.sub; simplified and moved most lemmas on sub from Sublist_Order to Sublist; Sublist_Order merely contains ord and order instances for sub plus some lemmas on the strict part of the order

base Sublist_Order on Sublist (using a simplified form of embedding as sublist relation)

dropped ord and bot instance for list prefixes (use locale interpretation instead, which allows users to decide what order to use on lists)

more lemmas on suffixes and embedding

changed arguement order of suffixeq (to facilitate reading "suffixeq xs ys" as "xs is a (possibly empty) suffix of ys)

added embedding for lists (constant emb)

renamed (in Sublist): postfix ~> suffixeq, and dropped infix syntax >>=

renamed (in Sublist): prefix ~> prefixeq, strict_prefix ~> prefix

renamed theory List_Prefix into Sublist (since it is not only about prefixes)

compile

rearrange dependencies

renamed three BNF/(co)datatype-related commands

tuned boundary cases of command-line; adhoc removal of PDFs stemming from base sessions;

"isabelle logo" produces EPS and PDF format simultaneously; more robust invocation of epstopdf: avoid filter mode;

actually reset output when there is no valid command span here (especially relevant at very end of jEdit buffer, which lacks the terminating newline);

tuned proofs;

some parallel ML;

proper classpath on windows;

proper classpath for Java FX;

basic setup for HTML5 panel; more JFX_Thread.operations;

basic support for Java FX;

maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;

removed unused material;

discontinued complicated/unreliable notion of recent proofs within context;

central management of forked goals wrt. transaction id; clarified stable_exec_id: consider ragular failure as stable; more robust counting of forked proofs, with global reset after cancellation due to document editing;

merged

always register proofs, even for empty binding;

tuned signature;

made parser a bit more flexible

tuning

pad the selectors' list with default names