Proof mod.

Added new thms.

quiet_mode;

Tools/inductive_package.ML;

triple_swap;

Wrapper module for Konrad Slind's TFL package.

remoced old set_current_thy;

tuned messages;

intrs: names and atts;

tuned comments; tuned types;

tuned comments; intrs: names and atts; Isar outer syntax;

tuned comments;

intrs: provide names and atts;

cleaned comments;

tuned;

fixed named type infixes (actual BUG!);

updated isatool install;

-p option; -k option;

adapted isatool install;

improved isatool install;

tuned;

ML_PLATFORM;

ML_PLATFORM;

fixed @@;

fixed bib file

fixed;

new definition for nth. added warnings, if primrec definition is deleted from simpset.

useless relic

arith_tac

tuned;

common qed and end of proofs;

* New bounded quantifier syntax (input only): ! x < y. P, ! x <= y. P, ? x < y. P, ? x <= y. P

New bounded quantifier syntax: !x<i. P etc

added new theory Yahalom_Bad

added new theory Yahalom_Bad

exchanged the order of Gets and Notes in datatype event

fixed thm_name again;

Theory.sign_of;

xnum token class;

xstr token class;

Theory.sign_of;

fixed axclass_tac;

tuned;

Theory.sign_of;

qualify Theory.sign_of etc.;

fixed msg;

tuned msg;

axclass_tac lost an argument;

HOL/typedef: fixed type inference for representing set; AxClass.axclass_tac lost the theory argument;

rep_datatype: '_i' version, attributes, outer syntax;

local open OuterParse;

actually check non-emptiness theorem; added typedef_proof(_i); 'typedef' outer syntax;

fixed typedef representing set;

adapted rep_datatype;

added dest_mem;

theory data; attributes for class axioms; instance_subclass/arity_proof(_i); expand_classes proof method; 'axclass' / 'instance' outer syntax;

adapted AxClass.add_axclass; PureThy.get_thm axioms;

tuned msgs; removed verbose flag;

tuned;

cleaned comments;