isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

re-organized some hyperreal and real lemmas
2003-12-25, by paulson
list_all2_nthD no good as [intro?]
2003-12-24, by kleing
list_all2_mono should not be [trans]
2003-12-23, by kleing
reorganised complex arithmetic
2003-12-23, by paulson
removing real_of_posnat
2003-12-23, by paulson
converting Hyperreal/NthRoot to Isar
2003-12-23, by paulson
converting Complex/Complex.ML to Isar
2003-12-23, by paulson
deleting redundant theorems
2003-12-23, by paulson
new theorems
2003-12-23, by paulson
tidying up hcomplex arithmetic
2003-12-23, by paulson
renaming some theorems
2003-12-23, by paulson
type hcomplex is now in class field
2003-12-23, by paulson
more ML bindings
2003-12-23, by paulson
added some [intro?] and [trans] for list_all2 lemmas
2003-12-23, by kleing
Updated proofs due to changes in Set.thy.
2003-12-22, by nipkow
converted Complex/NSComplex to Isar script
2003-12-22, by paulson
removal of the abel_cancel simproc for hypreal
2003-12-22, by paulson
downgrading abel_cancel
2003-12-22, by paulson
new binding
2003-12-22, by paulson
simplifying
2003-12-22, by paulson
moving HyperArith0.ML to other theories
2003-12-22, by paulson
removing obsolete bindings
2003-12-22, by paulson
tidying of HOL/Auth esp Guard lemmas
2003-12-21, by paulson
removed insert_Diff_single from simpset because it interfered with Auth :-(
2003-12-21, by nipkow
tidying first part of HyperArith0.ML, using generic lemmas
2003-12-19, by paulson
minor tweaks
2003-12-19, by paulson
type hypreal is an ordered field
2003-12-19, by paulson
*** empty log message ***
2003-12-19, by nipkow
tidied
2003-12-18, by paulson
*** empty log message ***
2003-12-18, by nipkow

less more | (0) -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle