Mercurial
Mercurial
>
repos
>
isabelle
/ graph
summary

shortlog

changelog
 graph 
tags

bookmarks

branches

files

gz

help
less
more

(0)
10000
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.
Implemented mechanism for attaching auxiliary code to consts_code and
20050712, by berghofe
small text mod
20050711, by nipkow
Fixed some problems with the signal handler.
20050711, by quigley
Improved implementation of Defs.is_overloaded.
20050711, by obua
Some changes to allow mutually recursive, overloaded functions with same name.
20050708, by berghofe
added Davenport reference
20050708, by nipkow
moved Davenport citation to Main, removed author list
20050708, by nipkow
moved gcd to new GCD.thy
20050708, by nipkow
proof needed updating because of arith
20050708, by nipkow
changed imports due to new GCD.thy
20050708, by nipkow
Used to be in Library/Primes
20050708, by nipkow
fix typo
20050708, by huffman
replaced old continuity rules with new lemma cont2cont_lift_case
20050708, by huffman
simplified proof of ifte_thms, removed ifte_simp
20050708, by huffman
renamed upE1 to upE; added simp rule cont2cont_flift1
20050708, by huffman
renamed upE1 to upE
20050708, by huffman
define 'a u with datatype package;
20050708, by huffman
added lemmas sinl_defined_iff sinr_defined_iff, sinl_eq_sinr, sinr_eq_sinl; added more simp rules; cleaned up
20050708, by huffman
add lemma eq_sprod
20050708, by huffman
add lemma eq_cprod
20050708, by huffman
removed obsolete continuity theorems
20050707, by huffman
define lift type using pcpodef; cleaned up
20050707, by huffman
cleaned up
20050707, by huffman
fixes to work with UU_reorient_simproc
20050707, by huffman
fixes to work with UU_reorient_simproc
20050707, by huffman
fixes to work with UU_reorient_simproc
20050707, by huffman
1) all theorems in Orderings can now be given as a parameter
20050707, by obua
use theorem ch2ch_cont
20050707, by huffman
inserted basic relevancechecking code, WHICH ONLY WORKS FOR 1ST SUBGOAL
20050707, by paulson
updated comment
20050707, by paulson
add UU_reorient_simproc
20050707, by huffman
use theorems ch2ch_cont, cont2contlubE
20050707, by huffman
add lemmas ch2ch_cont and cont2contlubE
20050707, by huffman
Preparations for interpretation of locales in locales.
20050707, by ballarin
takes & in premises apart now.
20050707, by nipkow
linear arithmetic is more powerful now
20050707, by nipkow
linear arithmetic now takes "&" in assumptions apart.
20050707, by nipkow
Used to be part of Finite_Set (or was it SetInterval?)
20050707, by nipkow
fixed antiquotation;
20050706, by wenzelm
removed timers;
20050706, by wenzelm
debug: exception_trace;
20050706, by wenzelm
finish: Output.accumulated_time;
20050706, by wenzelm
dest_parsers: sort result;
20050706, by wenzelm
added time_accumulator and accumulated_time supercede
20050706, by wenzelm
added full_prop_of: includes tpairs;
20050706, by wenzelm
tuned eq_ix;
20050706, by wenzelm
Context.check_thy;
20050706, by wenzelm
tuned forall_elim_var(s): avoid expensive Term.add_vars;
20050706, by wenzelm
tuned;
20050706, by wenzelm
Thm.full_prop_of;
20050706, by wenzelm
check_thy: less invocations, less verbose;
20050706, by wenzelm
* Pure: Output.time_accumulator;
20050706, by wenzelm
isatool fixheaders;
20050706, by wenzelm
tuned msg;
20050706, by wenzelm
ThyInfo.time_use root;
20050706, by wenzelm
added output_buffer;
20050706, by wenzelm
added write_list, append_list;
20050706, by wenzelm
tuned write: use File.write_list;
20050706, by wenzelm
tuned maxidx;
20050706, by wenzelm
tuned maxidx_of_typ/typs/term;
20050706, by wenzelm
less
more

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