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

merged

indexed document

Simplified some proofs, deleting a lot of strange unused material at the end of the theory.

fight spurious nitpick timeouts

reverted a87e49f4336d -- overwriting of data entries yields to merge problems later

more docs

more docs

docs

tidied

docs

docs about registering a BNF