104 |
104 |
105 notation (xsymbols) |
105 notation (xsymbols) |
106 iff (infixr "\<longleftrightarrow>" 25) |
106 iff (infixr "\<longleftrightarrow>" 25) |
107 |
107 |
108 nonterminal letbinds and letbind |
108 nonterminal letbinds and letbind |
109 nonterminal case_syn and cases_syn |
109 nonterminal case_pat and case_syn and cases_syn |
110 |
110 |
111 syntax |
111 syntax |
112 "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
112 "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
113 |
113 |
114 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
114 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
115 "" :: "letbind => letbinds" ("_") |
115 "" :: "letbind => letbinds" ("_") |
116 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
116 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
117 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10) |
117 "_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" [0, 10] 10) |
118 |
118 |
119 "_case_syntax":: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) |
119 "_case_syntax" :: "['a, cases_syn] => 'b" ("(case _ of/ _)" 10) |
120 "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) |
120 "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ =>/ _)" 10) |
121 "" :: "case_syn => cases_syn" ("_") |
121 "" :: "case_syn => cases_syn" ("_") |
122 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
122 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
|
123 "_strip_positions" :: "'a => case_pat" ("_") |
|
124 |
|
125 syntax (xsymbols) |
|
126 "_case1" :: "[case_pat, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
123 |
127 |
124 translations |
128 translations |
125 "THE x. P" == "CONST The (%x. P)" |
129 "THE x. P" == "CONST The (%x. P)" |
126 |
130 |
127 print_translation {* |
131 print_translation {* |
128 [(@{const_syntax The}, fn [Abs abs] => |
132 [(@{const_syntax The}, fn [Abs abs] => |
129 let val (x, t) = atomic_abs_tr' abs |
133 let val (x, t) = atomic_abs_tr' abs |
130 in Syntax.const @{syntax_const "_The"} $ x $ t end)] |
134 in Syntax.const @{syntax_const "_The"} $ x $ t end)] |
131 *} -- {* To avoid eta-contraction of body *} |
135 *} -- {* To avoid eta-contraction of body *} |
132 |
|
133 syntax (xsymbols) |
|
134 "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
|
135 |
136 |
136 notation (xsymbols) |
137 notation (xsymbols) |
137 All (binder "\<forall>" 10) and |
138 All (binder "\<forall>" 10) and |
138 Ex (binder "\<exists>" 10) and |
139 Ex (binder "\<exists>" 10) and |
139 Ex1 (binder "\<exists>!" 10) |
140 Ex1 (binder "\<exists>!" 10) |