src/HOL/Nominal/nominal_fresh_fun.ML
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