a faster proof

removed genelim.ML;

thm, thms;

added print_thm;

made SML/NJ happy;

added oo, ooo (*concatenation: 2 and 3 args*);

Attribute.tthms_of; Theory.copy;

Attribute.tthms_of;

Attribute.thms_of;

Classical.setup, attrib_setup;

attrib_setup: rulify;

attrib_setup;

all modifiers turned into attributes; realistic method syntax; smart_simp method;

tuned attribute names; all modifiers turned into attributes; realistic method syntax;

several args parsers; realistic syntax; tuned;

tuned names;

renamed tac / etac to refine / then_refine;

add print_theorems; print_thms: handle attributes; renamed tac / etac to refine / then_refine; tuned comments; load arg: name;

add print_theorems; print_thms: handle attributes;

several args parsers; realistic syntax; attributes: transfer, RS, APP, where, standard, elimify;

several args parsers; include positions; misc tuning;

removed args, args1, thm_xname; fixed nat: Symbol.explode; name / xname: include sym_ident; keyword_symid: include ident; tuned atom_arg; support nested args;

replaced is_symid by is_sid;

renamed init_context to init;

renamed init_context to init; added read_termTs; added declare_thm;

structure PureIsar;

removed lift_modifier; removed fail; added tthms_of; added print_tthm; tuned rule;

Attribute.thms_of;

Scan.read;

added read;