equal
deleted
inserted
replaced
144 |
144 |
145 defs |
145 defs |
146 Let_def: "Let s f == f(s)" |
146 Let_def: "Let s f == f(s)" |
147 if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)" |
147 if_def: "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)" |
148 |
148 |
149 arbitrary_def: "False ==> arbitrary == (THE x. False)" |
149 finalconsts |
150 -- {* @{term arbitrary} is completely unspecified, but is made to appear as a |
150 "op =" |
151 definition syntactically *} |
151 "op -->" |
152 |
152 The |
|
153 arbitrary |
153 |
154 |
154 subsubsection {* Generic algebraic operations *} |
155 subsubsection {* Generic algebraic operations *} |
155 |
156 |
156 axclass zero < type |
157 axclass zero < type |
157 axclass one < type |
158 axclass one < type |