src/HOL/NSA/HyperDef.thy
2009-05-11 haftmann 2009-05-11 qualified names for Lin_Arith tactics and simprocs
2009-05-11 haftmann 2009-05-11 tuned interface of Lin_Arith
2009-04-28 haftmann 2009-04-28 stripped class recpower further
2009-04-27 haftmann 2009-04-27 cleaned up theory power further
2009-04-23 haftmann 2009-04-23 adaptions due to rearrangment of power operation
2009-03-04 huffman 2009-03-04 declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s
2008-10-10 haftmann 2008-10-10 `code func` now just `code`
2008-07-11 huffman 2008-07-11 instance real_field < field_char_0; instance star :: (field_char_0) field_char_0
2008-07-03 huffman 2008-07-03 move nonstandard analysis theories to NSA directory