| Sat, 23 Mar 2013 17:11:06 +0100 |
haftmann |
tuned proof
|
changeset |
files
|
| Sat, 23 Mar 2013 17:11:06 +0100 |
haftmann |
locales for abstract orders
|
changeset |
files
|
| Sat, 23 Mar 2013 07:30:53 +0100 |
krauss |
merged
|
changeset |
files
|
| Fri, 22 Mar 2013 00:39:16 +0100 |
krauss |
added rudimentary induction rule for partial_function (heap)
|
changeset |
files
|
| Fri, 22 Mar 2013 00:39:14 +0100 |
krauss |
allow induction predicates with arbitrary arity (not just binary)
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move connected to HOL image; used to show intermediate value theorem
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move continuous and continuous_on to the HOL image; isCont is an abbreviation for continuous (at x) (isCont is now restricted to a T2 space)
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
clean up lemma_nest_unique and renamed to nested_sequence_unique
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
introduct the conditional_complete_lattice type class; generalize theorems about real Sup and Inf to it
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
generalize Bfun and Bseq to metric spaces; Bseq is an abbreviation for Bfun
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move first_countable_topology to the HOL image
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move metric_space to its own theory
|
changeset |
files
|
| Fri, 22 Mar 2013 10:41:42 +0100 |
hoelzl |
move topological_space to its own theory
|
changeset |
files
|
| Thu, 21 Mar 2013 16:58:14 +0100 |
wenzelm |
proper metric for blanks -- NB: 70f7483df9cb discontinues coincidence of char_width with space width;
|
changeset |
files
|
| Thu, 21 Mar 2013 16:35:53 +0100 |
wenzelm |
eliminated char_width_int to avoid unclear rounding;
|
changeset |
files
|
| Thu, 21 Mar 2013 10:05:03 +0100 |
nipkow |
proofs depend only on constraints, not on def of L WHILE
|
changeset |
files
|
| Wed, 20 Mar 2013 15:35:35 +0100 |
blanchet |
use the right role for SPASS hypotheses
|
changeset |
files
|
| Wed, 20 Mar 2013 14:56:30 +0100 |
kleing |
soundness statement as in type system
|
changeset |
files
|
| Wed, 20 Mar 2013 11:32:16 +0100 |
kleing |
add label for referencing in semantics book
|
changeset |
files
|
| Wed, 20 Mar 2013 11:16:31 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 19 Mar 2013 21:35:15 +0100 |
nipkow |
get rid of xcolor warnings
|
changeset |
files
|
| Tue, 19 Mar 2013 15:59:58 +0100 |
traytel |
extended stream library
|
changeset |
files
|
| Tue, 19 Mar 2013 14:04:53 +0100 |
kleing |
export datatype definition which gets expanded too much in antiquotation
|
changeset |
files
|
| Tue, 19 Mar 2013 14:07:13 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Tue, 19 Mar 2013 13:19:21 +0100 |
Andreas Lochbihler |
add induction rule for partial_function (tailrec)
|
changeset |
files
|