2014-09-09 blanchet set 'fundef_cong' attribute also for (co)datatypes with no live type variables
2014-09-09 blanchet ported IArray to new datatypes
2014-09-09 blanchet prevent infinite loop when type variables are of a non-'type' sort
2014-09-09 blanchet tuned code
2014-09-09 blanchet ported MicroJava to new datatypes
2014-09-09 blanchet rename_tac'd scrips
2014-09-09 blanchet ported Unix to new datatypes
2014-09-09 blanchet ported Isar_Examples to new datatypes
2014-09-09 blanchet ported Decision_Procs to new datatypes
2014-09-09 blanchet ported Induct to new datatypes
2014-09-09 blanchet half-ported Imperative HOL to new datatypes
2014-09-09 blanchet generalized 'datatype' LaTeX antiquotation and added 'codatatype'
2014-09-09 blanchet tuned messages
2014-09-09 blanchet rename_tac'd scripts
2014-09-09 blanchet reverted 83a8570b44bc, which was a misunderstanding
2014-09-09 blanchet rename_tac'd script
2014-09-09 blanchet ported Bali to new datatypes
2014-09-09 blanchet rename_tac'd scripts
2014-09-09 blanchet use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-09-09 nipkow merged
2014-09-09 nipkow enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
2014-09-09 steckerm Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
2014-09-08 blanchet more docs
2014-09-08 blanchet more documentation
2014-09-08 blanchet made 'lifting' plugin more robust
2014-09-08 blanchet tuned command descriptions
2014-09-08 blanchet generate better internal names, with name of the target type in it
2014-09-08 blanchet removed comment (yes, this is different -- add_typedef_global will fail in a locale with assumptions)
2014-09-08 blanchet added flag to 'typedef' to allow concealed definitions
2014-09-08 blanchet ported old Nominal to use new datatypes
2014-09-08 traytel made tactic even more robust w.r.t. dead variables
2014-09-08 blanchet made N2M work with sort constraints (cf. TODO)
2014-09-08 blanchet compile
2014-09-08 blanchet honour sorts in N2M
2014-09-08 blanchet proper sort constraints in map and rel theorems
2014-09-08 blanchet made new countable tactic work with sorts other than 'type'
2014-09-08 blanchet adapted examples to latest changes
2014-09-08 blanchet made code work also in the presence of deads
2014-09-08 blanchet export right sorts
2014-09-08 blanchet test sorts
2014-09-08 blanchet use right sort constraints
2014-09-08 blanchet never include hidden names -- these cannot be referenced afterward
2014-09-08 blanchet use compatibility layer
2014-09-08 blanchet made SML/NJ happire
2014-09-08 blanchet export useful functions for users of (co)recursors
2014-09-08 blanchet improved caching
2014-09-08 blanchet compile
2014-09-08 blanchet wildcards in plugins
2014-09-08 blanchet improved 'datatype_compat' further for recursion through functions
2014-09-08 blanchet no type-based lookup -- these fail in the general, ambiguous case
2014-09-08 blanchet tuning
2014-09-08 blanchet more examples/tests
2014-09-08 blanchet tuned docs
2014-09-08 blanchet properly note theorems for split recursors
2014-09-08 blanchet tuning
2014-09-08 blanchet updated docs
2014-09-08 blanchet extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
2014-09-08 blanchet tuning
2014-09-08 blanchet export one more ML function
2014-09-08 blanchet tuning
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip