| Thu, 01 Feb 2024 17:06:40 +0100 |
traytel |
made lift_bnf more robust for abstract types with 'phantom' type variables
|
file |
diff |
annotate
|
| Mon, 27 Jun 2022 15:54:18 +0200 |
traytel |
strict bounds for BNFs (by Jan van Brügge)
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
consolidated names and operations
|
file |
diff |
annotate
|
| Fri, 14 Aug 2020 14:40:24 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 15 Mar 2020 13:41:33 +0100 |
traytel |
remove Thm.transfer workaround made obsplete by cf2406e654cf
|
file |
diff |
annotate
|
| Fri, 28 Feb 2020 21:23:11 +0100 |
traytel |
tuned lift_bnf's user interface for quotients
|
file |
diff |
annotate
|
| Mon, 24 Feb 2020 21:46:45 +0100 |
traytel |
lift BNF witnesses for quotients (unless better ones are specified by the user)
|
file |
diff |
annotate
|
| Sun, 19 Jan 2020 07:50:35 +0100 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
file |
diff |
annotate
|
| Tue, 07 Jan 2020 14:58:01 +0100 |
traytel |
eliminated one redundant proof obligation in lift_bnf for quotients
|
file |
diff |
annotate
|
| Tue, 10 Dec 2019 01:06:39 +0100 |
traytel |
extension of lift_bnf to support quotient types
|
file |
diff |
annotate
|
| Tue, 10 Dec 2019 01:06:39 +0100 |
traytel |
unfold intermediate (internal) pred definitions
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 21:36:42 +0200 |
traytel |
store the unfolded definitions of the lifted bnf constants under "_def" name
|
file |
diff |
annotate
|
| Tue, 19 Apr 2016 13:05:50 +0200 |
traytel |
unfold internal definitions before emitting a proof obligation
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2016 08:38:50 +0200 |
traytel |
tuned interface
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 08:00:33 +0100 |
blanchet |
nicer error
|
file |
diff |
annotate
|
| Mon, 14 Mar 2016 21:37:49 +0100 |
blanchet |
generalized ML function
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Tue, 12 Jan 2016 09:28:08 +0100 |
traytel |
more careful witness' type analysis
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 22:44:07 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 22:30:41 +0200 |
wenzelm |
proper option, not catch-all pattern;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 20:55:22 +0200 |
wenzelm |
misc tuning and clarification;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 16:47:00 +0200 |
traytel |
unfold intermediate definitions (stemming from composition) in lifted bnf operations
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 20:46:33 +0200 |
traytel |
new command for lifting BNF structure over typedefs
|
file |
diff |
annotate
|