50 local |
50 local |
51 |
51 |
52 consts |
52 consts |
53 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
53 If :: "[bool, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
54 |
54 |
|
55 |
55 subsubsection {* Additional concrete syntax *} |
56 subsubsection {* Additional concrete syntax *} |
|
57 |
|
58 const_syntax (output) |
|
59 "op =" (infix "=" 50) |
|
60 |
|
61 abbreviation |
|
62 not_equal :: "['a, 'a] => bool" (infixl "~=" 50) |
|
63 "x ~= y == ~ (x = y)" |
|
64 |
|
65 const_syntax (output) |
|
66 not_equal (infix "~=" 50) |
|
67 |
|
68 const_syntax (xsymbols) |
|
69 Not ("\<not> _" [40] 40) |
|
70 "op &" (infixr "\<and>" 35) |
|
71 "op |" (infixr "\<or>" 30) |
|
72 "op -->" (infixr "\<longrightarrow>" 25) |
|
73 not_equal (infix "\<noteq>" 50) |
|
74 |
|
75 const_syntax (HTML output) |
|
76 Not ("\<not> _" [40] 40) |
|
77 "op &" (infixr "\<and>" 35) |
|
78 "op |" (infixr "\<or>" 30) |
|
79 not_equal (infix "\<noteq>" 50) |
|
80 |
|
81 abbreviation (iff) |
|
82 iff :: "[bool, bool] => bool" (infixr "<->" 25) |
|
83 "A <-> B == A = B" |
|
84 |
|
85 const_syntax (xsymbols) |
|
86 iff (infixr "\<longleftrightarrow>" 25) |
|
87 |
56 |
88 |
57 nonterminals |
89 nonterminals |
58 letbinds letbind |
90 letbinds letbind |
59 case_syn cases_syn |
91 case_syn cases_syn |
60 |
92 |
61 syntax |
93 syntax |
62 "_not_equal" :: "['a, 'a] => bool" (infixl "~=" 50) |
|
63 "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
94 "_The" :: "[pttrn, bool] => 'a" ("(3THE _./ _)" [0, 10] 10) |
64 |
95 |
65 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
96 "_bind" :: "[pttrn, 'a] => letbind" ("(2_ =/ _)" 10) |
66 "" :: "letbind => letbinds" ("_") |
97 "" :: "letbind => letbinds" ("_") |
67 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
98 "_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _") |
83 [("The", fn [Abs abs] => |
113 [("The", fn [Abs abs] => |
84 let val (x,t) = atomic_abs_tr' abs |
114 let val (x,t) = atomic_abs_tr' abs |
85 in Syntax.const "_The" $ x $ t end)] |
115 in Syntax.const "_The" $ x $ t end)] |
86 *} |
116 *} |
87 |
117 |
88 syntax (output) |
|
89 "=" :: "['a, 'a] => bool" (infix 50) |
|
90 "_not_equal" :: "['a, 'a] => bool" (infix "~=" 50) |
|
91 |
|
92 syntax (xsymbols) |
118 syntax (xsymbols) |
93 Not :: "bool => bool" ("\<not> _" [40] 40) |
|
94 "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) |
|
95 "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30) |
|
96 "op -->" :: "[bool, bool] => bool" (infixr "\<longrightarrow>" 25) |
|
97 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
|
98 "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
119 "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
99 "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
120 "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
100 "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
121 "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
101 "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
122 "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
102 (*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \<orelse> _")*) |
123 (*"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ \<orelse> _")*) |
103 |
124 |
104 syntax (xsymbols output) |
|
105 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
|
106 |
|
107 syntax (HTML output) |
125 syntax (HTML output) |
108 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
|
109 Not :: "bool => bool" ("\<not> _" [40] 40) |
|
110 "op &" :: "[bool, bool] => bool" (infixr "\<and>" 35) |
|
111 "op |" :: "[bool, bool] => bool" (infixr "\<or>" 30) |
|
112 "_not_equal" :: "['a, 'a] => bool" (infix "\<noteq>" 50) |
|
113 "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
126 "ALL " :: "[idts, bool] => bool" ("(3\<forall>_./ _)" [0, 10] 10) |
114 "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
127 "EX " :: "[idts, bool] => bool" ("(3\<exists>_./ _)" [0, 10] 10) |
115 "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
128 "EX! " :: "[idts, bool] => bool" ("(3\<exists>!_./ _)" [0, 10] 10) |
116 |
129 |
117 syntax (HOL) |
130 syntax (HOL) |
118 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
131 "ALL " :: "[idts, bool] => bool" ("(3! _./ _)" [0, 10] 10) |
119 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
132 "EX " :: "[idts, bool] => bool" ("(3? _./ _)" [0, 10] 10) |
120 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
133 "EX! " :: "[idts, bool] => bool" ("(3?! _./ _)" [0, 10] 10) |
121 |
|
122 abbreviation (iff) |
|
123 iff :: "[bool, bool] => bool" (infixr "<->" 25) |
|
124 "A <-> B == A = B" |
|
125 |
|
126 abbreviation (xsymbols) |
|
127 iff1 (infixr "\<longleftrightarrow>" 25) |
|
128 "A \<longleftrightarrow> B == A <-> B" |
|
129 |
134 |
130 |
135 |
131 subsubsection {* Axioms and basic definitions *} |
136 subsubsection {* Axioms and basic definitions *} |
132 |
137 |
133 axioms |
138 axioms |