Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScriptenabled browsers.
fixed deps;
20000621, by wenzelm
fixed deps;
20000621, by wenzelm
fixed deps;
20000621, by wenzelm
new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
20000621, by paulson
new theorem UN_empty; it and Un_empty inserted by AddIffs
20000621, by paulson
generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
20000621, by paulson
tidied; weakened the (impossible) premises of setsum_UN_disjoint
20000621, by paulson
new module for heaps
20000620, by paulson
now uses the heap data structure for BEST_FIRST
20000620, by paulson
new file heap.ML
20000620, by paulson
changed the Schubert Steamroller proof
20000620, by paulson
another brick in the wall
20000620, by paulson
changed a step for the improved rules for setsum
20000620, by paulson
deleted a step made redundant by the improved rules for setsum
20000620, by paulson
replaced the useless [p]subset_insertD by [p]subset_insert_iff
20000620, by paulson
now setsum f A = 0 unless A is finite
20000620, by paulson
now setsum f A = 0 unless A is finite; proved setsum_cong
20000620, by paulson
real simprocs
20000616, by paulson
fixed for removal of subset_empty
20000616, by paulson
this proof needs more detail
20000616, by paulson
uncommented the last 2 examples; tidied
20000616, by paulson
new lemma real_minus_diff_eq
20000616, by paulson
fixed the installation of linear arithmetic for the reals
20000616, by paulson
some missing simprules for integer linear arithmetic
20000616, by paulson
tidied for new card_seteq
20000616, by paulson
subset_empty is no longer a simprule
20000616, by paulson
renamed psubset_card > psubset_card_mono
20000616, by paulson
Finally "AddEs [equalityE]" is IN and "AddDs [equals0D, sym RS equals0D]" is OUT
20000616, by paulson
inserted some "addsimps [subset_empty]"; also tidied (a lot)
20000616, by paulson
tracing flag for arith_tac
20000616, by paulson
Now also proves monotonicity when in quick_and_dirty mode.
20000615, by berghofe
tidied
20000614, by paulson
full_rename_numerals > rename_numerals; tidied
20000614, by paulson
a big tidyup
20000614, by paulson
installing the cancel_numerals and combine_numerals simprocs
20000614, by paulson
tuned tappl syntax;
20000614, by wenzelm
theorems [cases type: bool] = case_split;
20000614, by wenzelm
full_rename_numerals > rename_numerals; tidied
20000614, by paulson
tidied a proof using new lemmas for signs of products
20000614, by paulson
new lemmas for signs of products
20000614, by paulson
new default simprules for m*n = 0
20000614, by paulson
tuned;
20000613, by wenzelm
rename @case to _case_syntax (improves on lowlevel errors);
20000613, by wenzelm
updated;
20000613, by wenzelm
qed_spec_mp: strip_shyps_warning;
20000613, by wenzelm
* browser info session directories are now selfcontained (may be put
20000609, by wenzelm
prf_open/close;
20000608, by wenzelm
replacing 0hr by (0::hypreal)
20000607, by paulson
minor tuning for pdf documents
20000607, by kleing
tidied
20000607, by paulson
provide TAGS file for Isabelle sources;
20000607, by wenzelm
string syntax: allow \\ \" \\n only;
20000607, by wenzelm
update_thy_only: setmp Thm.trace_simp false;
20000607, by wenzelm
renamed mktags to maketags;
20000607, by wenzelm
generate TAGS file for Isabelle sources;
20000607, by wenzelm
Removed cp / mkdir commands for graph browser files.
20000607, by berghofe
Exported system_command.
20000607, by berghofe
Removed codebase attribute from applet_pages.
20000607, by berghofe
Reorganized graph stuff.
20000607, by berghofe
First round of changes, towards installation of simprocs
20000607, by paulson
less
more

(0)
3000
1000
300
100
60
+60
+100
+300
+1000
+3000
+10000
+30000
tip