Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/HOL/Decision_Procs/Dense_Linear_Order.thy
2010-03-18
blanchet
2010-03-18
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
file
|
diff
|
annotate
2010-02-19
haftmann
2010-02-19
moved remaning class operations from Algebras.thy to Groups.thy
file
|
diff
|
annotate
2010-02-10
haftmann
2010-02-10
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
file
|
diff
|
annotate
2010-02-10
haftmann
2010-02-10
moved constants inverse and divide to Ring.thy
file
|
diff
|
annotate
2010-02-08
haftmann
2010-02-08
dropped accidental duplication of "lin" prefix from cs. 108662d50512
file
|
diff
|
annotate
2010-02-05
haftmann
2010-02-05
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
file
|
diff
|
annotate
2010-01-28
haftmann
2010-01-28
new theory Algebras.thy for generic algebraic structures
file
|
diff
|
annotate
2009-07-23
wenzelm
2009-07-23
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
file
|
diff
|
annotate
2009-04-29
haftmann
2009-04-29
farewell to class recpower
file
|
diff
|
annotate
2009-04-05
chaieb
2009-04-05
fixed usage of rational constants
file
|
diff
|
annotate
2009-03-27
haftmann
2009-03-27
merged
file
|
diff
|
annotate
2009-03-27
haftmann
2009-03-27
normalized imports
file
|
diff
|
annotate
2009-03-26
wenzelm
2009-03-26
interpretation/interpret: prefixes are mandatory by default;
file
|
diff
|
annotate
2009-03-22
haftmann
2009-03-22
distributed contents of theory Arith_Tools to theories Int, IntDiv and NatBin accordingly
file
|
diff
|
annotate
2009-03-16
wenzelm
2009-03-16
simplified method setup;
file
|
diff
|
annotate
2009-03-13
wenzelm
2009-03-13
unified type Proof.method and pervasive METHOD combinators;
file
|
diff
|
annotate
2009-03-11
hoelzl
2009-03-11
Updated paths in Decision_Procs comments and NEWS
file
|
diff
|
annotate
2009-02-09
chaieb
2009-02-09
A generic decision procedure for linear rea arithmetic and normed vector spaces
file
|
diff
|
annotate
2009-02-06
haftmann
2009-02-06
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
file
|
diff
|
annotate
|
base