| author | wneuper <Walther.Neuper@jku.at> |
| Sun, 09 Oct 2022 07:44:22 +0200 | |
| changeset 60565 | f92963a33fe3 |
| parent 60500 | 59a3af532717 |
| child 60660 | c4b24621077e |
| permissions | -rw-r--r-- |
| walther@60329 | 1 |
(* Title: Knowledge/root.sml |
| 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 ------------------------------"; |
| Walther@60565 | 18 |
val t = TermC.parse_test @{context} "sqrt 1";
|
| Walther@60500 | 19 |
val SOME (t',_) = rewrite_set_ ctxt false Root_erls t; |
| walther@59868 | 20 |
if UnparseC.term t' = "1" then () else error "root.sml: diff.behav. sqrt 1"; |
| neuper@42395 | 21 |
|
| Walther@60565 | 22 |
val t = TermC.parse_test @{context} "sqrt (- 1)";
|
| Walther@60500 | 23 |
val NONE = rewrite_set_ ctxt false Root_erls t; |
| neuper@37906 | 24 |
|
| Walther@60565 | 25 |
val t = TermC.parse_test @{context} "sqrt 0";
|
| Walther@60500 | 26 |
val SOME (t',_) = rewrite_set_ ctxt false Root_erls t; |
| walther@59868 | 27 |
if UnparseC.term t' = "0" then () else error "root.sml: diff.behav. sqrt 1"; |
| neuper@42395 | 28 |