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

improved case unfolding

switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.

tuned syntax: K_record is now an authentic constant

tuned: now using function package

transfer_tac accepts also HOL equations as theorems

shifted min/max to class order

tuned

added class tutorial

code generator changes

generate page labels

definition lookup via terms, not names. Methods "relation" and "lexicographic_order" do not depend on "termination" setup.

declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)

trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions