half-ported Imperative HOL to new datatypes

generalized 'datatype' LaTeX antiquotation and added 'codatatype'

tuned messages

rename_tac'd scripts

reverted 83a8570b44bc, which was a misunderstanding

rename_tac'd script

ported Bali to new datatypes

rename_tac'd scripts

use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries

merged

enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc

Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new

more docs

more documentation

made 'lifting' plugin more robust

tuned command descriptions

generate better internal names, with name of the target type in it

removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)

added flag to 'typedef' to allow concealed definitions

ported old Nominal to use new datatypes

made tactic even more robust w.r.t. dead variables

made N2M work with sort constraints (cf. TODO)

compile

honour sorts in N2M

proper sort constraints in map and rel theorems

made new countable tactic work with sorts other than 'type'

adapted examples to latest changes

made code work also in the presence of deads

export right sorts

test sorts

use right sort constraints

never include hidden names -- these cannot be referenced afterward

use compatibility layer

made SML/NJ happire

export useful functions for users of (co)recursors

improved caching

compile

wildcards in plugins

improved 'datatype_compat' further for recursion through functions

no type-based lookup -- these fail in the general, ambiguous case

tuning

more examples/tests

tuned docs

properly note theorems for split recursors

tuning

updated docs

extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions

tuning

export one more ML function

tuning

more compatibility documentation

refactored MaSh files to avoid regenerating exports on each eval

added missing 'transpose'

the kind is now always the empty string -- can no longer distinguish between user theorems and package theorems in a semi-reliable way

made tactic more robust w.r.t. dead variables

restrictive options for class dependencies

separated class_deps command into separate file

Added translation for lambda expressions in terms.

explicit theory with additional, less commonly used list operations

generalized

theory about sum and product on function bodies

theory about lexicographic ordering on functions

added various facts

Generalised card_length_listsum to all m

added lemma

updated docs

pretend code generation is a ctr_sugar plugin

updated docs

added 'plugins' option to control which hooks are enabled

introduced mechanism to filter interpretations

fixed infinite loops in 'register' functions + more uniform API

named interpretations

centralized and cleaned up naming handling

cleanup Wfrec; introduce dependent_wf/wellorder_choice

tuned Nitpick and Refute examples, which are too slow on some testing machines

tweaked setup for datatype realizer

renamed internal constant

moved code around

tuned size function generation

tuning

introduced local interpretation mechanism for BNFs, to solve issues with datatypes in locales

tuned ctr_sugar database handling

tuned BNF database handling

intelligible errors instead of tactic failures

reenabled yet another example

made new tactic even more robust

reenabled more examples

fixed tactic for n-way mutual recursion, n >= 4 (balanced conjunctions confuse the tactic)

reintroduced more examples

improved tactic further

reenabled example

improved new countability tactic

'prove_sorry' is too dangerous here -- the tactic is sometimes applied to non-theorems

more robust exception handling

added tests for new 'countable_datatype' proof method

lessen the burden on the caller: sort where necessary in n2m

added compatibility function

added countable tactic for new-style datatypes

tuning

registered 'typerep' as countable again

moved old datatype material around

removed vacuous theorem references

commented out failing tactic (now that 'typerep' is defined using the new package

tuned imports

use 'datatype_new'

use 'datatype_new' in 'Main'

take out 'x = C' of the simplifier for unit types

giving up calling 'datatype_compat' in a locale -- causes trouble with extensions

ported 'Statespace' to support new datatypes as well

use 'datatype_new' in Quickcheck examples

more compatibility functions

codatatypes are not datatypes