moved theorem tags from Drule to PureThy; replaced kind attribute by kind string; tuned name_multi: index > 1 only; added note_thmss_qualified (from Isar/locale.ML);

added ProofContext.pprint_context (depends on ProofContext.debug);

moved theorem tags from Drule to PureThy;

tidying up SPASS output

tidying

better reporting

Interface to access the specification of a named locale.

Added new file Tools/ATP/reduce_axiomsN.ML

Added in new file Tools/ATP/reduce_axiomsN.ML

Changed codes that call relevance filter.

Relevance filtering. Has replaced the previous version.

interrupt_timeout now raises Interrupt instead of SML90.Interrupt

smaller example to prevent timeout

Fixed bug in code generator for primitive definitions that caused dependencies to get mixed up.

Inductive sets with no introduction rules are now allowed as well.

added definition(_i);

renamed export to export_standard (again!), because it includes Drule.local_standard'; added abs_def (from locale.ML);

ProofContext.export_standard;

tuned atomize_cterm; added reverse_atomize_term/tac;

turned abstract_term into ProofContext.abs_def; ProofContext.export_standard;

added constant definition; tuned interfaces; tuned;

added 'definition'; 'spezification': optional fixes;

tuned comment;

export name_multi;

abs_def: improved error;

ObjectLogic.atomize_cterm;

updated;

works with DPLL solver now

the additional freshness-condition in the one-induction is not needed anywhere.

fixed code_generate syntax;