equal
deleted
inserted
replaced
22 |
22 |
23 abbreviation (xsymbols) |
23 abbreviation (xsymbols) |
24 square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) |
24 square :: "'a::power => 'a" ("(_\<twosuperior>)" [1000] 999) |
25 "x\<twosuperior> == x^2" |
25 "x\<twosuperior> == x^2" |
26 |
26 |
27 abbreviation (latex output) |
27 const_syntax (latex output) |
28 square1 ("(_\<twosuperior>)" [1000] 999) |
28 square ("(_\<twosuperior>)" [1000] 999) |
29 "square1 x == x^2" |
29 |
30 |
30 const_syntax (HTML output) |
31 abbreviation (HTML output) |
31 square ("(_\<twosuperior>)" [1000] 999) |
32 square2 ("(_\<twosuperior>)" [1000] 999) |
|
33 "square2 x == x^2" |
|
34 |
32 |
35 |
33 |
36 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} |
34 subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*} |
37 |
35 |
38 declare nat_0 [simp] nat_1 [simp] |
36 declare nat_0 [simp] nat_1 [simp] |