added snippets

simplify "Process" example further

simplify "Process" example

full name of a type as key in bnf table

fixed bug with one-value codatatype "codata 'a dead_foo = A"

tuning

fixed and reenabled "corecs" theorems

fixed and enabled generation of "coiters" theorems, including the recursive case

generate "fld_unf_corecs" as well

reactivated generation of "coiters" theorems

use map_id, not map_id', to allow better composition

open typedefs everywhere in the package

open typedef for datatypes

fixed and enabled iterator/recursor theorems

renamed for consistency

oops

tuning

for compatiblity with old datatype package: not only "recs" with "s", but also "iters" and their "fld_"/"unf_" variants

fixed bug with one-value types with phantom type arguments

imported patch debugging

repaired "nofail4" example

renamed xxxBNF to pre_xxx

fixed handling of map of "fun"

comment out code that's not ready

tuning

construct the right iterator theorem in the recursive case

some work on coiter tactic

more sugar on codatatypes

define corecursors

define coiterators

TODO

tuning

completed iter/rec proofs

TODOs

implemented "mk_iter_or_rec_tac"

generate iter/rec goals

repaired constant types

some work towards iterator and recursor properties

tuning

correctly curry recursor arguments

added high-level recursor, not yet curried

merged

tuned proofs;

postpone update of text overview panel after incoming session edits, to improve reactivity of editing massive theories like src/HOL/Multivariate_Analysis;

more explicit Delay operations;

tuned proofs;

clearer names for functions in Quickcheck's narrowing engine

merged

tuned latex

lattice instances for option type

combinator Option.these

adjusted examples

countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"

handle type constructors not known to be a BNF using the DEADID BNF

respect order of/additional type variables supplied by the user in fixed point constructions;

gracefully handle shadowing case (fourth step of sugar localization)

careful about constructor types w.r.t. fake context (third step of localization)

read the real types off the constant types, rather than using the fake parser types (second step of sugar localization)

tuning

use "add_type" rather than "add_types_global"

don't throw away the context when hacking the theory (first step to localize the sugar code)

tuning

introduced and used "mk_Freesss", and simplified "mk_Freess(')"

construct high-level iterator RHS

option for discarding build results, enabled in particular for Isabelle_makeall

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;