equal
deleted
inserted
replaced
58 is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*) |
58 is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*) |
59 |
59 |
60 is'_multUnordered:: "real => bool" ("_ is'_multUnordered") |
60 is'_multUnordered:: "real => bool" ("_ is'_multUnordered") |
61 is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*) |
61 is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*) |
62 is'_polyexp :: "real => bool" ("_ is'_polyexp") |
62 is'_polyexp :: "real => bool" ("_ is'_polyexp") |
63 |
|
64 Expand'_binoms |
|
65 :: "['y, |
|
66 'y] => 'y" |
|
67 ("((Script Expand'_binoms (_ =))// (_))" 9) |
|
68 |
63 |
69 subsection \<open>theorems not yet adopted from Isabelle\<close> |
64 subsection \<open>theorems not yet adopted from Isabelle\<close> |
70 axiomatization where (*.not contained in Isabelle2002, |
65 axiomatization where (*.not contained in Isabelle2002, |
71 stated as axioms, TODO: prove as theorems; |
66 stated as axioms, TODO: prove as theorems; |
72 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*) |
67 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*) |