Achim D. Brucker
|
bf691e04a0
|
Fixed markdown.
|
2018-06-27 00:40:43 +01:00 |
Achim D. Brucker
|
4fe36e9ad4
|
Fixed markdown.
|
2018-06-26 17:28:21 +01:00 |
Achim D. Brucker
|
8a5e954215
|
Prefixed examples to avoid naming conflicts with consuming theories.
|
2018-06-25 19:02:35 +01:00 |
Achim D. Brucker
|
a069d566f8
|
Bug fix: wrong order of default variables.
|
2018-06-25 19:00:09 +01:00 |
Achim D. Brucker
|
09aa5120f5
|
Renamed ._ (_.) to .._ (_..) to avoid conflict with common match pattern.
|
2018-06-25 18:59:05 +01:00 |
Achim D. Brucker
|
ec1db40bd9
|
Renamed example definitions to avoid name clashes with consuming theories.
|
2018-06-24 21:39:50 +01:00 |
Achim D. Brucker
|
e53d1bcb01
|
Renamed symtab storing tvar information.
|
2018-06-24 21:06:06 +01:00 |
Achim D. Brucker
|
479c60b2f3
|
Added input syntax for specifying the last type variable of a type constructor.
|
2018-06-24 13:32:11 +01:00 |
Achim D. Brucker
|
d0fc49b78c
|
Improved documentation.
|
2018-06-24 00:40:52 +01:00 |
Achim D. Brucker
|
45e55cf4e7
|
Implemented possibility to specify a sort (type class) for default variables.
|
2018-06-24 00:08:15 +01:00 |
Achim D. Brucker
|
ce7e3896b3
|
Fixed markdown.
|
2018-06-22 17:34:52 +01:00 |
Achim D. Brucker
|
868cfc53a3
|
Added reference to the isabelle-hacks repository.
|
2018-06-22 16:51:47 +01:00 |
Achim D. Brucker
|
39ca1b5dc0
|
Moved hide_tvar_subst_ast_tr into structure Hide_Tvar.
|
2018-06-22 16:07:03 +01:00 |
Achim D. Brucker
|
b493001ea6
|
Added asserts for type variable customization.
|
2018-06-22 15:56:20 +01:00 |
Achim D. Brucker
|
251414e8b4
|
Cleanup of parse translation hide_tvar_subst_ast_tr.
|
2018-06-22 15:45:29 +01:00 |
Achim D. Brucker
|
3c1b07e065
|
Introduced ._ and _. notation to override first/last default type variables.
|
2018-06-22 15:43:07 +01:00 |
Achim D. Brucker
|
54d9b20cc4
|
Implemented print mode (only apply print translation if default types match).
|
2018-06-21 23:08:39 +01:00 |
Achim D. Brucker
|
66307c1c2b
|
Made top-level user interface more consistent.
|
2018-06-21 21:34:57 +01:00 |
Achim D. Brucker
|
92ea551113
|
Support type synonyms as output notation.
|
2018-06-21 21:24:20 +01:00 |
Achim D. Brucker
|
66101d2527
|
Changed styntax for type wildcard from __ to (_).
|
2018-06-20 10:57:09 +01:00 |
Achim D. Brucker
|
8e9a19266a
|
Support type synonyms as input notation.
|
2018-06-18 13:32:18 +01:00 |
Achim D. Brucker
|
3b0a88dfa6
|
Renamed theories to comply to Isabelle's naming convention.
|
2018-06-18 09:50:22 +01:00 |
Achim D. Brucker
|
9bfbf12444
|
Register print translation automatically.
|
2018-06-18 05:10:10 +01:00 |
Achim D. Brucker
|
eed51f4515
|
Theory restructuring.
|
2018-06-17 23:17:51 +01:00 |
Achim D. Brucker
|
4bc432fcbb
|
First implementation of the corresponding parse translation.
|
2018-06-17 22:58:59 +01:00 |
Achim D. Brucker
|
40082ac32b
|
Updated shorthand notation.
|
2018-06-17 22:57:09 +01:00 |
Achim D. Brucker
|
2577669f5f
|
Added hiding_type_variables.thy.
|
2018-06-17 21:38:59 +01:00 |
Achim D. Brucker
|
0051269b36
|
Fixed markdown.
|
2018-06-17 21:33:19 +01:00 |
Achim D. Brucker
|
66f94a0bd5
|
Initial commit.
|
2018-06-17 21:17:41 +01:00 |
Achim D. Brucker
|
6c1e607542
|
Added author information.
|
2018-06-17 08:38:49 +01:00 |
Achim D. Brucker
|
347a428ef1
|
Added dependency information (excluding Isabelle/HOL).
|
2018-06-17 00:16:00 +01:00 |
Achim D. Brucker
|
9403f7449c
|
Initial commit.
|
2018-06-17 00:00:46 +01:00 |
Achim D. Brucker
|
5c1e76c1eb
|
Added assert.thy to README.
|
2018-06-16 23:57:35 +01:00 |
Achim D. Brucker
|
4bb87cec6e
|
Initial commit.
|
2018-06-16 23:54:08 +01:00 |
Achim D. Brucker
|
13f2bfe8a9
|
Initial commit.
|
2018-06-14 19:22:45 +01:00 |