added adm.ML;

tuned;

tuned simp trace;

*** empty log message ***

Removed spurious blank. Updated proof because of HOL change.

Updated proofs

For each datatype `t' there is now a theorem `split_t_case' of the form P(t_case f1 ... fn x) = ((!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1))& ... (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))) The simplifier now reduces !x. (..x.. & x = t & ..x..) --> P x to (..t.. & ..t..) --> P t (and similarly for t=x).

fixed spaces in qed;

debugging concerning sort variables theorems are now proved immediately after generating the syntax

PureThy.add_store_axioms_i;