52 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
52 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
53 |
53 |
54 |
54 |
55 subsubsection {* Additional concrete syntax *} |
55 subsubsection {* Additional concrete syntax *} |
56 |
56 |
57 const_syntax (output) |
57 notation (output) |
58 "op =" (infix "=" 50) |
58 "op =" (infix "=" 50) |
59 |
59 |
60 abbreviation |
60 abbreviation |
61 not_equal :: "['a, 'a] => bool" (infixl "~=" 50) |
61 not_equal :: "['a, 'a] => bool" (infixl "~=" 50) |
62 "x ~= y == ~ (x = y)" |
62 "x ~= y == ~ (x = y)" |
63 |
63 |
64 const_syntax (output) |
64 notation (output) |
65 not_equal (infix "~=" 50) |
65 not_equal (infix "~=" 50) |
66 |
66 |
67 const_syntax (xsymbols) |
67 notation (xsymbols) |
68 Not ("\<not> _" [40] 40) |
68 Not ("\<not> _" [40] 40) |
69 "op &" (infixr "\<and>" 35) |
69 "op &" (infixr "\<and>" 35) |
70 "op |" (infixr "\<or>" 30) |
70 "op |" (infixr "\<or>" 30) |
71 "op -->" (infixr "\<longrightarrow>" 25) |
71 "op -->" (infixr "\<longrightarrow>" 25) |
72 not_equal (infix "\<noteq>" 50) |
72 not_equal (infix "\<noteq>" 50) |
73 |
73 |
74 const_syntax (HTML output) |
74 notation (HTML output) |
75 Not ("\<not> _" [40] 40) |
75 Not ("\<not> _" [40] 40) |
76 "op &" (infixr "\<and>" 35) |
76 "op &" (infixr "\<and>" 35) |
77 "op |" (infixr "\<or>" 30) |
77 "op |" (infixr "\<or>" 30) |
78 not_equal (infix "\<noteq>" 50) |
78 not_equal (infix "\<noteq>" 50) |
79 |
79 |
80 abbreviation (iff) |
80 abbreviation (iff) |
81 iff :: "[bool, bool] => bool" (infixr "<->" 25) |
81 iff :: "[bool, bool] => bool" (infixr "<->" 25) |
82 "A <-> B == A = B" |
82 "A <-> B == A = B" |
83 |
83 |
84 const_syntax (xsymbols) |
84 notation (xsymbols) |
85 iff (infixr "\<longleftrightarrow>" 25) |
85 iff (infixr "\<longleftrightarrow>" 25) |
86 |
86 |
87 |
87 |
88 nonterminals |
88 nonterminals |
89 letbinds letbind |
89 letbinds letbind |
213 if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match |
213 if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match |
214 else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
214 else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T); |
215 in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end; |
215 in map (tr' o Sign.const_syntax_name (the_context ())) ["HOL.one", "HOL.zero"] end; |
216 *} -- {* show types that are presumably too general *} |
216 *} -- {* show types that are presumably too general *} |
217 |
217 |
218 const_syntax |
218 notation |
219 uminus ("- _" [81] 80) |
219 uminus ("- _" [81] 80) |
220 |
220 |
221 const_syntax (xsymbols) |
221 notation (xsymbols) |
222 abs ("\<bar>_\<bar>") |
222 abs ("\<bar>_\<bar>") |
223 const_syntax (HTML output) |
223 notation (HTML output) |
224 abs ("\<bar>_\<bar>") |
224 abs ("\<bar>_\<bar>") |
225 |
225 |
226 |
226 |
227 subsection {* Fundamental rules *} |
227 subsection {* Fundamental rules *} |
228 |
228 |