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