added auxiliary lemmas for proof tools

dropped preorders, unified syntax

minimal import

dropped HOL.ML

tuned

updated Alice version;

IntInf.fromInt;

added "set" supression

added test about "set" supression

polished all proofs and made the theory "self-contained"

deleted some unnecessary type-annotations

tuned some of the proofs and added the lemma fresh_bool

tuned allpairs

tuned some proofs and changed variable names in some definitions of Nominal.thy

added allpairs

removed obsolete get_sg;

explicit treatment of legacy_features;

Fixing bugs in the partial-typed and fully-typed translations

Removal of dead code

tuned some proofs in CR and properly included CR_Takahashi

removed obsolete induct/simp tactic;

alternative and much simpler proof for Church-Rosser of Beta-Reduction

use correct email program for sunbroy2

removed legacy ML files;

eliminated unnamed infixes;

added header;

added header; tuned presentation;

added

removed lagacy ML files;

updated;

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