use names like 'rec_mytype' and 'case_mytype' in old datatype package as well, to avoid a mixture

use right local theory -- shows up when 'no_discs_sels' is set

compatibility names

use new selector support to define 'the', 'hd', 'tl'

transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'

avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'

tuned code

more 'ctr_sugar' modernization

tuning

ported predicate compiler to 'ctr_sugar' * * * ported predicate compiler to 'ctr_sugar', part 2

updated docs

generate 'fundec_cong' attribute for new-style (co)datatypes * * * compile

got rid of dynamic scoping the easy way

removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)

more liberal merging of BNFs and constructor sugar * * * make sure that the cache doesn't produce 'DUP's

se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets

have the same no-update semantics for 'case' as for 'Ctr_Sugar' and BNF data (this might not be the final word on the matter, but using a consistent policy seems like a good idea)

Mac OS X Lion (macbroy6) is baseline for portable executables; fringe platforms are unsupported;

"no_memory" option for the simplifier trace to bypass memoization

tuned

merged

seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;

make triple-sure that the future scheduler is properly shutdown (see also 702278df3b57);

discontinued axiomatic 'classes', 'classrel', 'arities';

updated keywords;

more explicit axiomatization;

prefer vacuous definitional type classes over axiomatic ones;

more explicit axiomatization;

prefer vacuous definitional type classes over axiomatic ones;

comments;

removed rotten code;

more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example: lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))" using [[simp_depth_limit = 1]] apply simp oops

merged

improved lin.arith. for terms involving division

restoring ancient string_classes option

method names in instance declarations are always unqualified

dropped legacy finally

tidied messy proofs

minimal document;

removed junk;

merged

check scalable fonts;

do *not* enforce scalable fonts for T1 encoding, instead rely on cm-super fonts, which also provide underscore for non-tt font;

yet another attempt at actual underscore; enforce scalable fonts for T1 encoding;

build up preprocessing context only once

tuned

disabled counterexample output for now; confusing because often incorrect

more indexing