sane version of read_termTs (proper freeze); added read_terms, cert_terms;

read_instantiations: proper type-inference with fixed variables, infer parameter types as well; gen_prep_registration: removed unused read_terms (dead code!); tuned;

added paramify_vars; infer: replace params uniformly (notably freeze);

def_simproc(_i): proper ProofContext.read/cert_terms;

simplified ProofContext.read_termTs;

simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)

initial commit

faster proof of wf_eq_minimal

export get_sort (belongs to Syntax module);

TypeExt.decode_term;

added decode_term (belongs to Syntax module);

tuned the setup of fresh_fun

defs are added to code data

repaired value restriction problem

reverted to classical syntax for K_record

tuned

Interpretation equations applied to attributes

Interpretation equations applied to attributes; code cleanup in read_instantiations

Modified eqvt_tac to avoid failure due to introduction rules whose premises contain variables that do not occur in the conclusion.

clarifed

modify fresh_fun_simp to ease debugging

updated code generator

updated

adds extracted program to code theorem table

unfold attribute now also accepts HOL equations

added more stuff

add definitions explicitly to code generator table

cleared dead code

moved axclass module closer to core system

Isar definitions are now added explicitly to code theorem table