2007-04-25 berghofe 2007-04-25 Moved functions infer_intro_vars, arities_of, params_of, and partition_rules to inductive_package.ML.
2007-04-25 berghofe 2007-04-25 Added functions arities_of, params_of, partition_rules, and infer_intro_vars (from inductive_realizer.ML).
2007-04-25 berghofe 2007-04-25 eqvt_tac now instantiates introduction rules before applying them.
2007-04-24 narboux 2007-04-24 update fresh_fun_simp for debugging purposes
2007-04-24 narboux 2007-04-24 fixes last commit
2007-04-24 narboux 2007-04-24 add two lemmas dealing with freshness on permutations.
2007-04-24 berghofe 2007-04-24 Added datatype_case.ML and nominal_fresh_fun.ML.
2007-04-24 berghofe 2007-04-24 Added datatype_case.
2007-04-24 berghofe 2007-04-24 Added intro / elim rules for prod_case.
2007-04-24 berghofe 2007-04-24 sum_case is now authentic.
2007-04-24 berghofe 2007-04-24 Adapted to new parse translation for case expressions.
2007-04-24 berghofe 2007-04-24 Parse / print translations for nested case expressions, taken from Konrad Slind's TFL package.
2007-04-24 berghofe 2007-04-24 Streamlined datatype_codegen function using new datatype_of_case and datatype_of_constr functions.
2007-04-24 berghofe 2007-04-24 - 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.
2007-04-24 berghofe 2007-04-24 case constants are now authentic.
2007-04-24 narboux 2007-04-24 oups : wrong commit
2007-04-24 narboux 2007-04-24 adds op in front of an infix to fix SML compilation
2007-04-23 wenzelm 2007-04-23 sane version of read_termTs (proper freeze); added read_terms, cert_terms;
2007-04-23 wenzelm 2007-04-23 read_instantiations: proper type-inference with fixed variables, infer parameter types as well; gen_prep_registration: removed unused read_terms (dead code!); tuned;
2007-04-23 wenzelm 2007-04-23 added paramify_vars; infer: replace params uniformly (notably freeze);
2007-04-23 wenzelm 2007-04-23 def_simproc(_i): proper ProofContext.read/cert_terms;
2007-04-23 wenzelm 2007-04-23 simplified ProofContext.read_termTs;
2007-04-23 urbanc 2007-04-23 simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
2007-04-23 haftmann 2007-04-23 initial commit
2007-04-21 huffman 2007-04-21 faster proof of wf_eq_minimal
2007-04-21 wenzelm 2007-04-21 export get_sort (belongs to Syntax module);
2007-04-21 wenzelm 2007-04-21 TypeExt.decode_term;
2007-04-21 wenzelm 2007-04-21 added decode_term (belongs to Syntax module);
2007-04-21 urbanc 2007-04-21 tuned the setup of fresh_fun
2007-04-20 haftmann 2007-04-20 defs are added to code data
2007-04-20 haftmann 2007-04-20 repaired value restriction problem
2007-04-20 haftmann 2007-04-20 reverted to classical syntax for K_record
2007-04-20 haftmann 2007-04-20 tuned
2007-04-20 ballarin 2007-04-20 Interpretation equations applied to attributes
2007-04-20 ballarin 2007-04-20 Interpretation equations applied to attributes; code cleanup in read_instantiations
2007-04-20 berghofe 2007-04-20 Modified eqvt_tac to avoid failure due to introduction rules whose premises contain variables that do not occur in the conclusion.
2007-04-20 haftmann 2007-04-20 clarifed
2007-04-20 narboux 2007-04-20 modify fresh_fun_simp to ease debugging
2007-04-20 haftmann 2007-04-20 updated code generator
2007-04-20 haftmann 2007-04-20 updated
2007-04-20 haftmann 2007-04-20 adds extracted program to code theorem table
2007-04-20 haftmann 2007-04-20 unfold attribute now also accepts HOL equations
2007-04-20 haftmann 2007-04-20 added more stuff
2007-04-20 haftmann 2007-04-20 add definitions explicitly to code generator table
2007-04-20 haftmann 2007-04-20 cleared dead code
2007-04-20 haftmann 2007-04-20 moved axclass module closer to core system
2007-04-20 haftmann 2007-04-20 Isar definitions are now added explicitly to code theorem table
2007-04-20 haftmann 2007-04-20 improved case unfolding
2007-04-20 haftmann 2007-04-20 switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
2007-04-20 haftmann 2007-04-20 tuned syntax: K_record is now an authentic constant
2007-04-20 haftmann 2007-04-20 tuned: now using function package
2007-04-20 haftmann 2007-04-20 transfer_tac accepts also HOL equations as theorems
2007-04-20 haftmann 2007-04-20 shifted min/max to class order
2007-04-20 haftmann 2007-04-20 tuned
2007-04-20 haftmann 2007-04-20 added class tutorial
2007-04-20 haftmann 2007-04-20 code generator changes
2007-04-20 krauss 2007-04-20 generate page labels
2007-04-20 krauss 2007-04-20 definition lookup via terms, not names. Methods "relation" and "lexicographic_order" do not depend on "termination" setup.
2007-04-20 urbanc 2007-04-20 declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)
2007-04-19 paulson 2007-04-19 trying to make single-step proofs work better, especially if they contain abstraction functions. Uniform names for Skolem and Abstraction functions