| Sun, 15 Nov 2020 07:17:06 +0000 |
haftmann |
bundles for reflected term syntax
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 09:06:44 +0100 |
haftmann |
bundled syntax for state monad combinators
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2016 07:58:14 +0200 |
nipkow |
added [simp] lemmas
|
file |
diff |
annotate
|
| Thu, 05 Nov 2015 10:39:49 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 20:46:33 +0200 |
traytel |
use lift_bnf in an example
|
file |
diff |
annotate
|
| Mon, 06 Jul 2015 22:57:34 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 16:51:11 +0100 |
traytel |
alist is a BNF
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:20:45 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Tue, 28 Oct 2014 17:16:22 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 23:03:50 +0100 |
kuncar |
simplify proofs because of the stronger reflexivity prover
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
| Wed, 28 Mar 2012 10:02:22 +0200 |
bulwahn |
removing now redundant impl_of theorems in DAList
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 14:14:46 +0200 |
bulwahn |
association lists with distinct keys uses the quotient infrastructure to obtain code certificates;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 22:53:24 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 10:45:42 +0100 |
bulwahn |
renaming theory AList_Impl back to AList (reverting 1fec5b365f9b; AList with distinct key invariant is called DAList)
|
file |
diff |
annotate
|
| Tue, 17 Jan 2012 09:38:30 +0100 |
bulwahn |
renamed theory AList to DAList
|
file |
diff |
annotate
| base
|