| Wed, 11 Nov 2015 09:48:24 +0100 |
Andreas Lochbihler |
add various lemmas
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 05 Dec 2014 14:14:36 +0100 |
kuncar |
Workaround that allows us to execute lifted constants that have as a return type a datatype containing a subtype
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 15:03:21 +0100 |
Andreas Lochbihler |
more transfer rules
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 13:52:12 +0100 |
Andreas Lochbihler |
add parametricity rule for Ex1
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 13:51:16 +0100 |
Andreas Lochbihler |
add intro and elim rules for right_total
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 06:56:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 14:06:13 +0100 |
desharna |
Add plugin to generate transfer theorem for primrec and primcorec
|
file |
diff |
annotate
|
| Mon, 15 Dec 2014 07:20:48 +0100 |
blanchet |
renamed theory file
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 15:02:29 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:56 +0200 |
desharna |
generate 'corec_transfer' for codatatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:50 +0200 |
desharna |
generate 'ctor_rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Fri, 19 Sep 2014 10:40:56 +0200 |
traytel |
typo
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 11:20:59 +0200 |
blanchet |
tweaked setup for datatype realizer
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
file |
diff |
annotate
|
| Mon, 21 Jul 2014 17:51:29 +0200 |
Andreas Lochbihler |
add parametricity lemmas
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
merged two small theory files
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:18:10 +0200 |
blanchet |
fixed postprocessing of 'coinduct' formula to obtain right property format (without needless hypotheses)
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 17:57:56 +0200 |
kuncar |
predicator simplification rules: support also partially specialized types e.g. 'a * nat
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:27 +0200 |
blanchet |
qualify name
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 23:22:00 +0200 |
kuncar |
bi_unique and co. rules from the BNF hook must be introduced after bi_unique op= and co. rules are introduced
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:18 +0200 |
kuncar |
setup for Transfer and Lifting from BNF; tuned thm names
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:15 +0200 |
kuncar |
abstract Domainp in relator_domain rules => more natural statement of the rule
|
file |
diff |
annotate
|
| Thu, 10 Apr 2014 17:48:14 +0200 |
kuncar |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
killed a few 'metis' calls
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Fri, 28 Feb 2014 17:54:52 +0100 |
traytel |
load Metis a little later
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 16:48:15 +0100 |
kuncar |
transfer domain rule for special case of functions - was missing
|
file |
diff |
annotate
|