eliminated unnamed infixes;

renamed some old names Theory.xxx to Sign.xxx;

eliminated unnamed infixes; tuned ML setup;

added header;

eliminated unnamed infixes, tuned syntax;

clarified naming policy

clarified semantics of merge

moved stuff to Char_nat.thy

tuned

slightly tuned

replaced recdef by function

cleaned up code generator setup for int

added lemmatas

moved code generation pretty integers and characters to separate theories

updated doc

mk_const_def: Sign.intern_term (legacy);

renamed some old names Theory.xxx to Sign.xxx;

updated;

add the lemma supp_eqvt and put the right attribute

new lemma splice_length

fix sml compilation

Moved function params_of to inductive_package.ML.

Moved functions infer_intro_vars, arities_of, params_of, and partition_rules to inductive_package.ML.

Added functions arities_of, params_of, partition_rules, and infer_intro_vars (from inductive_realizer.ML).

eqvt_tac now instantiates introduction rules before applying them.

update fresh_fun_simp for debugging purposes

fixes last commit

add two lemmas dealing with freshness on permutations.

Added datatype_case.ML and nominal_fresh_fun.ML.

Added datatype_case.

Added intro / elim rules for prod_case.

sum_case is now authentic.

Adapted to new parse translation for case expressions.

Parse / print translations for nested case expressions, taken from Konrad Slind's TFL package.

Streamlined datatype_codegen function using new datatype_of_case and datatype_of_constr functions.

- Moved parse / print translations for case to datatype_case.ML - Added new functions datatype_of_constr and datatype_of_case to retrieve datatype corresponding to name of constructor or case combinator.

case constants are now authentic.

oups : wrong commit

adds op in front of an infix to fix SML compilation

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

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

nominal_inductive no longer proves equivariance.

add a tactic to generate fresh names

simplified ProofContext.infer_types(_pats);

Improved comments.

proper header, added regression tests

added temporary hack to avoid schematic goals in "termination".

Fixes for proof reconstruction, especially involving abstractions and definitions

export is_dummy_pattern;

lemma isCont_inv_fun is same as isCont_inverse_function

moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy

remove use of pos_boundedE

lemma geometric_sum no longer needs class division_by_zero

tuned proofs;

canonical merge operations

added print_indexname; tuned;

improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls

added a more usuable lemma for dealing with fresh_fun

generalized type of lemma geometric_sum

replaced read_term_legacy by read_prop_legacy; read: intern_skolem before type-inference (many workarounds!); read: reject_tvars; removed obsolete TypeInfer.logicT -- use dummyT; add_fixes: not constraints for external names;

removed obsolete redeclare_skolems;

read prop as prop, not term;

removed obsolete TypeInfer.logicT -- use dummyT;

avoid internal names;

tuned;

legacy_infer_term/prop -- including intern_term;

Thm.plain_prop_of;

added decode_types (from type_infer.ML); decode sorts: internalize here; tuned;

added read_term; adapted decoding of types/sorts;

added mixfixT (from type_infer.ML);

proper interface infer_types(_pat); Syntax.mixfixT; tuned;

Thm.fold_terms; Syntax.mixfixT;

removed unused Output.panic hook -- internal to PG wrapper;

moved get_sort to sign.ML; moved decode_types to Syntax/type_ext.ML; moved mixfixT to Syntax/mixfix.ML; proper infer_types, without decode/name lookup; tuned;

removed obsolete inferT_axm;

removed obsolete infer_types(_simult); read_sort/get_sort, read_def_terms: internal reorganization;

moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;

load type_infer.ML early;

adapted decode_type;