2007-05-21 narboux [Mon, 21 May 2007 16:19:56 +0200] rev 23054
change fresh_fun_simp to treat occurences in assumptions and try to solve the generated subgoals
src/HOL/Nominal/nominal_fresh_fun.ML

2007-05-20 huffman [Sun, 20 May 2007 18:48:52 +0200] rev 23053
define pi with THE instead of SOME; cleaned up
src/HOL/Hyperreal/Transcendental.thy

2007-05-20 huffman [Sun, 20 May 2007 17:49:10 +0200] rev 23052
add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
src/HOL/Hyperreal/Transcendental.thy

2007-05-20 huffman [Sun, 20 May 2007 17:30:21 +0200] rev 23051
add lemma power2_eq_imp_eq
src/HOL/Integ/NatBin.thy

2007-05-20 urbanc [Sun, 20 May 2007 13:39:46 +0200] rev 23050
added lemma for permutations on strings
src/HOL/Nominal/Nominal.thy

2007-05-20 huffman [Sun, 20 May 2007 10:13:06 +0200] rev 23049
moved sqrt lemmas from Transcendental.thy to NthRoot.thy
src/HOL/Hyperreal/NthRoot.thy src/HOL/Hyperreal/Transcendental.thy

2007-05-20 huffman [Sun, 20 May 2007 09:50:56 +0200] rev 23048
remove obsolete DERIV_ln lemmas
src/HOL/Hyperreal/Transcendental.thy

2007-05-20 huffman [Sun, 20 May 2007 09:21:04 +0200] rev 23047
add realpow_pos_nth2 back in
src/HOL/Hyperreal/NthRoot.thy

2007-05-20 huffman [Sun, 20 May 2007 09:05:44 +0200] rev 23046
add odd_real_root lemmas
src/HOL/Hyperreal/NthRoot.thy

2007-05-20 huffman [Sun, 20 May 2007 08:16:29 +0200] rev 23045
add lemmas about inverse functions; cleaned up proof of polar_ex
src/HOL/Hyperreal/Transcendental.thy