| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Mon, 26 Aug 2024 21:59:35 +0100 |
paulson |
More tidying of old proofs
|
file |
diff |
annotate
|
| Fri, 26 May 2023 15:44:59 +0200 |
desharna |
redefined FSet.fBall and FSet.fBex as abbreviations based on Set.Ball and Set.Bex
|
file |
diff |
annotate
|
| Tue, 10 Dec 2019 01:06:39 +0100 |
traytel |
extension of lift_bnf to support quotient types
|
file |
diff |
annotate
|
| Wed, 22 May 2019 22:18:45 +0200 |
Lars Hupel |
Finite_Map: move lemmas from LambdaAuth AFP entry
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 18 Nov 2018 18:07:51 +0000 |
haftmann |
removed legacy input syntax
|
file |
diff |
annotate
|
| Tue, 16 Oct 2018 18:34:44 +0200 |
Lars Hupel |
more material on finite maps
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 10:42:42 +0200 |
Lars Hupel |
material on finite sets
|
file |
diff |
annotate
|
| Sat, 25 Aug 2018 20:44:09 +0200 |
Lars Hupel |
material on finite maps
|
file |
diff |
annotate
|
| Fri, 17 Aug 2018 21:34:56 +0200 |
Lars Hupel |
Finite_Map: monotonicity
|
file |
diff |
annotate
|
| Mon, 18 Jun 2018 11:15:46 +0200 |
Lars Hupel |
material on finite sets and maps
|
file |
diff |
annotate
|
| Mon, 18 Jun 2018 10:50:24 +0200 |
Lars Hupel |
simplify parametricity proofs
|
file |
diff |
annotate
|
| Wed, 06 Jun 2018 11:12:37 +0200 |
nipkow |
Keep filter input syntax
|
file |
diff |
annotate
|
| Tue, 22 May 2018 11:08:37 +0200 |
nipkow |
First step to remove nonstandard "[x <- xs. P]" syntax: only input
|
file |
diff |
annotate
|
| Wed, 07 Mar 2018 19:02:22 +0100 |
wenzelm |
more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
|
file |
diff |
annotate
|
| Mon, 22 Jan 2018 15:06:38 +0100 |
Lars Hupel |
repair malformed fundef_cong rule
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 11 Aug 2017 16:54:49 +0200 |
Lars Hupel |
fmap :: size
|
file |
diff |
annotate
|
| Thu, 20 Jul 2017 15:41:01 +0200 |
Lars Hupel |
tuned code setup
|
file |
diff |
annotate
|
| Sun, 16 Jul 2017 23:47:21 +0200 |
Lars Hupel |
fmap is finite
|
file |
diff |
annotate
|
| Wed, 12 Jul 2017 11:33:32 +0200 |
Lars Hupel |
more material on finite maps
|
file |
diff |
annotate
|
| Wed, 12 Jul 2017 07:52:35 +0200 |
traytel |
redundant since c6714a9562ae
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 17:11:37 +0200 |
Lars Hupel |
more material on fmaps
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 16:12:36 +0200 |
Lars Hupel |
canonical representation for fmaps is fmlookup
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 15:34:35 +0200 |
Lars Hupel |
fmaps are countable
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Thu, 13 Oct 2016 15:43:15 +0200 |
Lars Hupel |
renamed lemma to a more consistent name
|
file |
diff |
annotate
|
| Thu, 13 Oct 2016 14:41:45 +0200 |
Lars Hupel |
tuned
|
file |
diff |
annotate
|
| Thu, 13 Oct 2016 14:15:34 +0200 |
Lars Hupel |
remove accidentally oops'ed (and wrong) lemma
|
file |
diff |
annotate
|
| Fri, 16 Sep 2016 18:44:18 +0200 |
Lars Hupel |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 22:41:05 +0200 |
Lars Hupel |
new type for finite maps; use it in HOL-Probability
|
file |
diff |
annotate
|