cleanup in datatype package

small type annotation fix

added hook for codegen_theorems.ML

adaptions to change in typedef_package.ML

added functions for definitional code generation

added definitional code generator module: codegen_theorems.ML

minor changes

exported specification names

minor extensions

pool of constants; definition expansion; current best settings

removed some illegal characters: they were crashing SML/NJ

Removal of unused code

Simplified version of Jia's filter. Now all constants are pooled, rather than relevance being compared against separate clauses. Rejects are no longer noted, and units cannot be added at the end.

renamed map_val to map_ran

added map_val, superseding map_at and substitute ----------------------------------------------------------------------

some internal cleanup

removed illegal character codes

simplified the proof at_fin_set_supp

changed abbreviation for "infinite" back to translation because something didn't work during (output).

lazy patterns in lambda abstractions

changed the it_prm proof to work for recursion

tuned some proofs

Removed occurrences of makestring, which does not exist in SML/NJ.

Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.

Replaced iteration combinator by recursion combinator.

detection of definitions of relevant constants

Only display atpset theorems if Output.show_debug_msgs is true.

added the first two simple proofs of the recursion combinator

comment fixed

Introduction of "whitelist": theorems forced past the relevance filter

Slight simplification of proofs

Removal of obsolete strategies. Initial support for locales: Frees and Consts treated similarly.

comment for conjI added

translations -> abbreviations (a cool feature)

fixed example;

mark_boundT: produce well-typed term;

subtract (op =); pretty_proof: no abbrevs;

avoid polymorphic equality; tuned;

avoid polymorphic equality; subtract (op =);

moved gen_eq_set to library.ML;

added ~$$ (negative literal); combinators: avoid code duplication; tuned extend_lexicon;

avoid polymorphic equality;

remove (op =); tuned;

gen_eq_set, remove (op =);

abbreviation upto, length;

added subtract; tuned;

subtract (op =);

remove (op =);

Now SML/NJ-friendly (IntInf)

Removal of unnecessary simprules: simproc cancel_numerals now works without add_Suc, while the reason for the horrible isolateSuc is not known.

interpret: Proof.assert_forward_or_chain;

subsetI is often necessary

Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer need to be outermost.

Tuned signature of Locale.add_locale(_i).

simplified mg_domain (use Sign.classes/arities_of); removed unused lift_local_theory_yield;

made $$ and "this" monomorphic (string);