3092 (map, set, predicator, relator, and cardinal bound) and asserts the BNF properties for |
3092 (map, set, predicator, relator, and cardinal bound) and asserts the BNF properties for |
3093 these constants as axioms. |
3093 these constants as axioms. |
3094 |
3094 |
3095 The syntactic entity \synt{target} can be used to specify a local context, |
3095 The syntactic entity \synt{target} can be used to specify a local context, |
3096 \synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable |
3096 \synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable |
3097 (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix} denotes the usual |
3097 (@{typ 'a}, @{typ 'b}, \ldots), \synt{mixfix} denotes the usual parenthesized |
3098 parenthesized mixfix notation @{cite "isabelle-isar-ref"}. |
3098 mixfix notation, and \synt{types} denotes a space-separated list of types |
|
3099 @{cite "isabelle-isar-ref"}. |
3099 |
3100 |
3100 The @{syntax plugins} option indicates which plugins should be enabled |
3101 The @{syntax plugins} option indicates which plugins should be enabled |
3101 (@{text only}) or disabled (@{text del}). By default, all plugins are enabled. |
3102 (@{text only}) or disabled (@{text del}). By default, all plugins are enabled. |
3102 |
3103 |
3103 Type arguments are live by default; they can be marked as dead by entering |
3104 Type arguments are live by default; they can be marked as dead by entering |