| author | Walther Neuper <wneuper@ist.tugraz.at> |
| Mon, 27 May 2019 19:28:40 +0200 | |
| changeset 59540 | 98298342fb6d |
| parent 59472 | 3e904f8ec16c |
| permissions | -rw-r--r-- |
| neuper@37906 | 1 |
(* theory collecting all knowledge defined so far |
| neuper@37906 | 2 |
WN.11.00 |
| neuper@37906 | 3 |
*) |
| neuper@37906 | 4 |
|
| neuper@41929 | 5 |
theory Isac |
| neuper@48880 | 6 |
imports "~~/src/Tools/isac/Frontend/Frontend" |
| wneuper@59425 | 7 |
PolyMinus PolyEq Vect DiffApp Biegelinie AlgEin InsSort |
| neuper@42280 | 8 |
DiophantEq Inverse_Z_Transform Test |
| neuper@48895 | 9 |
(*THIS WAITS UNITL Isabelle2013 (? how include into dependency graph?)..... |
| neuper@48895 | 10 |
..... GCD_Poly_FP*) |
| neuper@41929 | 11 |
begin |
| neuper@37906 | 12 |
|
| wneuper@59472 | 13 |
text \<open>dependencies alternative to those defined by R.Lang during his thesis: |
| neuper@37906 | 14 |
|
| neuper@37906 | 15 |
Poly Root |
| neuper@37906 | 16 |
|\__________ | |
| neuper@37906 | 17 |
| \ | |
| neuper@37906 | 18 |
| Rational | |
| neuper@37906 | 19 |
| | | |
| neuper@37906 | 20 |
PolyEq RatEq RootEq |
| neuper@37906 | 21 |
\ / \ / |
| neuper@37906 | 22 |
\ / \ / |
| neuper@37906 | 23 |
RatPolyEq RatRootEq etc. |
| wneuper@59472 | 24 |
\<close> |
| neuper@37954 | 25 |
|
| wneuper@59472 | 26 |
ML \<open>val version_isac = "isac version 120504 15:33";\<close> |
| wneuper@59540 | 27 |
ML \<open> |
| wneuper@59540 | 28 |
"~~~~~ fun xxx , args:"; val () = (); |
| wneuper@59540 | 29 |
\<close> ML \<open> |
| wneuper@59540 | 30 |
\<close> ML \<open> |
| wneuper@59540 | 31 |
"~~~~~ fun xxx , args:"; val () = (); |
| wneuper@59540 | 32 |
\<close> |
| neuper@42412 | 33 |
|
| neuper@37954 | 34 |
end |