haftmann [Sat, 23 Mar 2013 17:11:06 +0100] rev 51488
tuned proof
haftmann [Sat, 23 Mar 2013 17:11:06 +0100] rev 51487
locales for abstract orders
krauss [Sat, 23 Mar 2013 07:30:53 +0100] rev 51486
merged
krauss [Fri, 22 Mar 2013 00:39:16 +0100] rev 51485
added rudimentary induction rule for partial_function (heap)
krauss [Fri, 22 Mar 2013 00:39:14 +0100] rev 51484
allow induction predicates with arbitrary arity (not just binary)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51483
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51482
arcsin and arccos are continuous on {0 .. 1} (including the endpoints)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51481
move continuous_on_inv to HOL image (simplifies isCont_inverse_function)
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51480
move connected to HOL image; used to show intermediate value theorem
hoelzl [Fri, 22 Mar 2013 10:41:43 +0100] rev 51479
move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets