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;