Fri, 23 Apr 2010 13:58:14 +0200 | haftmann | more localization; factored out lemmas for division_ring | file | diff | annotate |
Thu, 18 Mar 2010 12:58:52 +0100 | blanchet | now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp" | file | diff | annotate |
Thu, 04 Mar 2010 18:42:39 +0100 | hoelzl | Add dense_le, dense_le_bounded, field_le_mult_one_interval. | file | diff | annotate |
Thu, 18 Feb 2010 14:21:44 -0800 | huffman | get rid of many duplicate simp rule warnings | file | diff | annotate |
Wed, 10 Feb 2010 14:12:02 +0100 | haftmann | moved lemma field_le_epsilon from Real.thy to Fields.thy | file | diff | annotate |
Wed, 10 Feb 2010 08:49:26 +0100 | haftmann | moved constants inverse and divide to Ring.thy | file | diff | annotate |
Mon, 08 Feb 2010 17:12:38 +0100 | haftmann | renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields | file | diff | annotate | base |