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