| author | Walther Neuper <walther.neuper@jku.at> |
| Thu, 09 Apr 2020 17:13:17 +0200 | |
| changeset 59861 | 65ec9f679c3f |
| parent 59196 | bf4a50413a0b |
| child 59868 | d77aa0992e0f |
| permissions | -rw-r--r-- |
| neuper@41943 | 1 |
(* Title: testexamples for Root, radicals |
| neuper@41943 | 2 |
Author: Walther Neuper |
| neuper@41943 | 3 |
(c) due to copyright terms |
| neuper@41943 | 4 |
*) |
| neuper@41943 | 5 |
"--------------------------------------------------------"; |
| neuper@41943 | 6 |
"table of contents --------------------------------------"; |
| neuper@41943 | 7 |
"--------------------------------------------------------"; |
| neuper@42395 | 8 |
"----------- rls Root_erls ------------------------------"; |
| neuper@41943 | 9 |
"--------------------------------------------------------"; |
| neuper@41943 | 10 |
"--------------------------------------------------------"; |
| neuper@41943 | 11 |
|
| neuper@42395 | 12 |
val thy = @{theory "Root"};
|
| neuper@48761 | 13 |
val ctxt = Proof_Context.init_global thy; |
| neuper@37906 | 14 |
|
| neuper@42395 | 15 |
"----------- rls Root_erls ------------------------------"; |
| neuper@42395 | 16 |
"----------- rls Root_erls ------------------------------"; |
| neuper@42395 | 17 |
"----------- rls Root_erls ------------------------------"; |
| neuper@37906 | 18 |
val t = str2term "sqrt 1"; |
| neuper@37926 | 19 |
val SOME (t',_) = rewrite_set_ thy false Root_erls t; |
| walther@59861 | 20 |
if UnparseC.term2str t' = "1" then () else error "root.sml: diff.behav. sqrt 1"; |
| neuper@42395 | 21 |
|
| wneuper@59196 | 22 |
val t = str2term "sqrt (-1)"; |
| neuper@37926 | 23 |
val NONE = rewrite_set_ thy false Root_erls t; |
| neuper@37906 | 24 |
|
| neuper@37906 | 25 |
val t = str2term "sqrt 0"; |
| neuper@37926 | 26 |
val SOME (t',_) = rewrite_set_ thy false Root_erls t; |
| walther@59861 | 27 |
if UnparseC.term2str t' = "0" then () else error "root.sml: diff.behav. sqrt 1"; |
| neuper@42395 | 28 |