src/HOL/Nominal/nominal_fresh_fun.ML
Thu, 24 May 2007 12:00:47 +0200 narboux add an option in fresh_fun_simp to prevent rewriting in assumptions
Mon, 21 May 2007 19:14:12 +0200 narboux search bottom up to get the inner fresh fun
Mon, 21 May 2007 16:19:56 +0200 narboux change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
Wed, 25 Apr 2007 15:38:56 +0200 narboux fix sml compilation
Tue, 24 Apr 2007 18:06:04 +0200 narboux update fresh_fun_simp for debugging purposes
Tue, 24 Apr 2007 14:01:23 +0200 narboux adds op in front of an infix to fix SML compilation
Fri, 20 Apr 2007 14:30:35 +0200 narboux modify fresh_fun_simp to ease debugging
Thu, 19 Apr 2007 16:27:53 +0200 narboux add a tactic to generate fresh names
less more (0) tip