src/HOL/Nominal/nominal_fresh_fun.ML
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2008-06-16 wenzelm 2008-06-16 pervasive RuleInsts;
2008-06-12 wenzelm 2008-06-12 use regular error function;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 auxiliary dynamic_thm(s) for fact lookup;
2007-09-08 urbanc 2007-09-08 some cleaning up
2007-08-14 wenzelm 2007-08-14 avoid low-level tsig;
2007-06-13 narboux 2007-06-13 generate_fresh works even if there is no free variable in the goal
2007-05-24 narboux 2007-05-24 fix a bug : the semantics of no_asm was the opposite
2007-05-24 narboux 2007-05-24 add an option in fresh_fun_simp to prevent rewriting in assumptions
2007-05-21 narboux 2007-05-21 search bottom up to get the inner fresh fun
2007-05-21 narboux 2007-05-21 change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
2007-04-25 narboux 2007-04-25 fix sml compilation
2007-04-24 narboux 2007-04-24 update fresh_fun_simp for debugging purposes
2007-04-24 narboux 2007-04-24 adds op in front of an infix to fix SML compilation
2007-04-20 narboux 2007-04-20 modify fresh_fun_simp to ease debugging
2007-04-19 narboux 2007-04-19 add a tactic to generate fresh names