equal
deleted
inserted
replaced
16 "n" <= "CONST of_nat n" |
16 "n" <= "CONST of_nat n" |
17 "n" <= "CONST int n" |
17 "n" <= "CONST int n" |
18 "n" <= "real n" |
18 "n" <= "real n" |
19 "n" <= "CONST real_of_nat n" |
19 "n" <= "CONST real_of_nat n" |
20 "n" <= "CONST real_of_int n" |
20 "n" <= "CONST real_of_int n" |
|
21 "n" <= "CONST of_real n" |
|
22 "n" <= "CONST complex_of_real n" |
21 |
23 |
22 (* append *) |
24 (* append *) |
23 syntax (latex output) |
25 syntax (latex output) |
24 "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65) |
26 "appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65) |
25 translations |
27 translations |