src/HOL/Tools/inductive_realizer.ML
2008-12-31 wenzelm 2008-12-31 eliminated OldTerm.add_term_free_names;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use exists_Const directly;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-11-16 wenzelm 2008-11-16 clarified Thm.proof_body_of vs. Thm.proof_of;
2008-11-15 wenzelm 2008-11-15 name_of_thm: Proofterm.fold_proof_atoms; Thm.proof_of returns proof_body;
2008-09-23 wenzelm 2008-09-23 Thm.proof_of;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-24 haftmann 2008-08-24 default replaces arbitrary
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-06-10 haftmann 2008-06-10 polished interface of datatype package
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-17 wenzelm 2008-04-17 prove_global: pass context;
2008-04-15 wenzelm 2008-04-15 PureThy.hide_fact;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-04-03 berghofe 2008-04-03 Added skip_mono flag to inductive definition package.
2008-03-29 wenzelm 2008-03-29 simplified PureThy.store_thm;
2008-03-29 wenzelm 2008-03-29 eliminated quiete_mode ref (turned into proper argument);
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2008-02-25 wenzelm 2008-02-25 inductive package: simplified group handling;
2008-01-26 wenzelm 2008-01-26 internal inductive: fresh theorem group;
2007-10-09 wenzelm 2007-10-09 AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-02 wenzelm 2007-10-02 tuned internal inductive interface;
2007-09-28 berghofe 2007-09-28 Adapted to changes in interface of add_inductive_i.
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-08-06 berghofe 2007-08-06 Added renaming function to prevent correctness proof for realizer of induction rule to fail because of name clashes between parameters and predicate variables.
2007-07-05 wenzelm 2007-07-05 renamed ObjectLogic.atomize_tac to ObjectLogic.atomize_prems_tac;
2007-07-05 wenzelm 2007-07-05 avoid polymorphic equality;
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-05 berghofe 2007-04-05 - Tried to make name_of_thm more robust against changes of the structure of proofs. - Now uses add_inductive_global rather than add_inductive_i for the definition of the realizability predicate.
2007-04-04 wenzelm 2007-04-04 rep_thm/cterm/ctyp: removed obsolete sign field;
2007-02-07 berghofe 2007-02-07 Adapted to new inductive definition package.
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-16 wenzelm 2006-11-16 moved some fundamental concepts to General/basics.ML;
2006-10-13 berghofe 2006-10-13 Moved old inductive package to old_inductive_package.ML
2006-10-10 haftmann 2006-10-10 gen_rem(s) abandoned in favour of remove / subtract
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list);
2006-06-07 wenzelm 2006-06-07 renamed Type.(un)varifyT to Logic.(un)varifyT; made (un)varify strict wrt. global context -- may use legacy_(un)varify as workaround;
2006-05-11 wenzelm 2006-05-11 avoid raw equality on type thm;
2006-04-30 wenzelm 2006-04-30 AxClass.axiomatize_arity_i;
2006-04-26 wenzelm 2006-04-26 tuned;
2006-02-15 wenzelm 2006-02-15 removed distinct, renamed gen_distinct to distinct;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-06 haftmann 2005-12-06 re-oriented some result tuples in PureThy
2005-12-01 haftmann 2005-12-01 oriented pairs theory * 'a to 'a * theory
2005-10-28 haftmann 2005-10-28 swapped add_datatype result
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-09-19 haftmann 2005-09-19 introduced AList module
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-05-31 wenzelm 2005-05-31 Theory.restore_naming;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Args.global_const (static binding!);
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.