| #
cf411881 |
|
28-Feb-2020 |
traytel <none@none> |
tuned lift_bnf's user interface for quotients
|
| #
113cbdbc |
|
24-Feb-2020 |
traytel <none@none> |
lift BNF witnesses for quotients (unless better ones are specified by the user)
|
| #
043c3b16 |
|
18-Jan-2020 |
traytel <none@none> |
new examples of BNF lifting across quotients using a new theory of confluence,
which simplifies the relator subdistributivity proof obligation
(a few new useful notions were added to HOL;
notably the symmetric and equivalence closures of a relation)
|
| #
3d6494dc |
|
07-Jan-2020 |
traytel <none@none> |
eliminated one redundant proof obligation in lift_bnf for quotients
|
| #
a794106c |
|
09-Dec-2019 |
traytel <none@none> |
extension of lift_bnf to support quotient types
|
| #
e661a369 |
|
09-Dec-2019 |
traytel <none@none> |
unfold intermediate (internal) pred definitions
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
43466b8c |
|
11-Jul-2017 |
traytel <none@none> |
store the unfolded definitions of the lifted bnf constants under "_def" name
|
| #
1d9f3775 |
|
19-Apr-2016 |
traytel <none@none> |
unfold internal definitions before emitting a proof obligation
|
| #
5dc803d8 |
|
13-Apr-2016 |
wenzelm <none@none> |
eliminated "xname" and variants;
|
| #
bf5ee1bb |
|
31-Mar-2016 |
traytel <none@none> |
tuned interface
|
| #
0a1b3fe0 |
|
22-Mar-2016 |
blanchet <none@none> |
nicer error
|
| #
e786a3b5 |
|
14-Mar-2016 |
blanchet <none@none> |
generalized ML function
|
| #
6b18406f |
|
16-Feb-2016 |
traytel <none@none> |
make predicator a first-class bnf citizen
|
| #
dcbe0bca |
|
12-Jan-2016 |
traytel <none@none> |
more careful witness' type analysis
|
| #
369e4785 |
|
13-Dec-2015 |
wenzelm <none@none> |
more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
|
| #
7fa8309e |
|
31-Aug-2015 |
wenzelm <none@none> |
misc tuning and simplification;
|
| #
b1457fe2 |
|
31-Aug-2015 |
wenzelm <none@none> |
proper option, not catch-all pattern;
|
| #
ea009ece |
|
31-Aug-2015 |
wenzelm <none@none> |
misc tuning and clarification;
|
| #
222d333a |
|
13-Aug-2015 |
traytel <none@none> |
unfold intermediate definitions (stemming from composition) in lifted bnf operations
|
| #
45936566 |
|
12-Aug-2015 |
traytel <none@none> |
new command for lifting BNF structure over typedefs
|