Mercurial
Mercurial
>
repos
>
isabelle
/ shortlog
summary
| shortlog |
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
files
|
gz
|
help
(0)
-3000
-1000
-300
-100
-50
-28
+28
+50
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
2000-06-21
paulson
new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
changeset
|
files
2000-06-21
paulson
new theorem UN_empty; it and Un_empty inserted by AddIffs
changeset
|
files
2000-06-21
paulson
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
changeset
|
files
2000-06-21
paulson
tidied; weakened the (impossible) premises of setsum_UN_disjoint
changeset
|
files
2000-06-20
paulson
new module for heaps
changeset
|
files
2000-06-20
paulson
now uses the heap data structure for BEST_FIRST
changeset
|
files
2000-06-20
paulson
new file heap.ML
changeset
|
files
2000-06-20
paulson
changed the Schubert Steamroller proof
changeset
|
files
2000-06-20
paulson
another brick in the wall
changeset
|
files
2000-06-20
paulson
changed a step for the improved rules for setsum
changeset
|
files
2000-06-20
paulson
deleted a step made redundant by the improved rules for setsum
changeset
|
files
2000-06-20
paulson
replaced the useless [p]subset_insertD by [p]subset_insert_iff
changeset
|
files
2000-06-20
paulson
now setsum f A = 0 unless A is finite
changeset
|
files
2000-06-20
paulson
now setsum f A = 0 unless A is finite; proved setsum_cong
changeset
|
files
2000-06-16
paulson
real simprocs
changeset
|
files
2000-06-16
paulson
fixed for removal of subset_empty
changeset
|
files
2000-06-16
paulson
this proof needs more detail
changeset
|
files
2000-06-16
paulson
uncommented the last 2 examples; tidied
changeset
|
files
2000-06-16
paulson
new lemma real_minus_diff_eq
changeset
|
files
2000-06-16
paulson
fixed the installation of linear arithmetic for the reals
changeset
|
files
2000-06-16
paulson
some missing simprules for integer linear arithmetic
changeset
|
files
2000-06-16
paulson
tidied for new card_seteq
changeset
|
files
2000-06-16
paulson
subset_empty is no longer a simprule
changeset
|
files
2000-06-16
paulson
renamed psubset_card -> psubset_card_mono
changeset
|
files
2000-06-16
paulson
Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
changeset
|
files
2000-06-16
paulson
inserted some "addsimps [subset_empty]"; also tidied (a lot)
changeset
|
files
2000-06-16
paulson
tracing flag for arith_tac
changeset
|
files
2000-06-15
berghofe
Now also proves monotonicity when in quick_and_dirty mode.
changeset
|
files
Loading...
(0)
-3000
-1000
-300
-100
-50
-28
+28
+50
+100
+300
+1000
+3000
+10000
+30000
tip