| Fri, 11 Apr 2014 22:53:33 +0200 |
nipkow |
made divide_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Fri, 20 Sep 2013 20:21:54 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 22 Mar 2013 10:41:43 +0100 |
hoelzl |
move connected to HOL image; used to show intermediate value theorem
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 09:51:34 +0100 |
bulwahn |
simplifying proof
|
file |
diff |
annotate
|
| Sun, 20 Nov 2011 21:05:23 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 10:36:17 -0800 |
huffman |
polished and converted some proofs to Isar style
|
file |
diff |
annotate
|
| Tue, 23 Feb 2010 17:33:03 +0100 |
hoelzl |
Moved old Integration to examples.
|
file |
diff |
annotate
| base
|