13 val ctxt = Proof_Context.init_global thy; |
13 val ctxt = Proof_Context.init_global thy; |
14 |
14 |
15 "----------- rls Root_erls ------------------------------"; |
15 "----------- rls Root_erls ------------------------------"; |
16 "----------- rls Root_erls ------------------------------"; |
16 "----------- rls Root_erls ------------------------------"; |
17 "----------- rls Root_erls ------------------------------"; |
17 "----------- rls Root_erls ------------------------------"; |
18 val t = TermC.str2term "sqrt 1"; |
18 val t = TermC.parse_test @{context} "sqrt 1"; |
19 val SOME (t',_) = rewrite_set_ ctxt false Root_erls t; |
19 val SOME (t',_) = rewrite_set_ ctxt false Root_erls t; |
20 if UnparseC.term t' = "1" then () else error "root.sml: diff.behav. sqrt 1"; |
20 if UnparseC.term t' = "1" then () else error "root.sml: diff.behav. sqrt 1"; |
21 |
21 |
22 val t = TermC.str2term "sqrt (- 1)"; |
22 val t = TermC.parse_test @{context} "sqrt (- 1)"; |
23 val NONE = rewrite_set_ ctxt false Root_erls t; |
23 val NONE = rewrite_set_ ctxt false Root_erls t; |
24 |
24 |
25 val t = TermC.str2term "sqrt 0"; |
25 val t = TermC.parse_test @{context} "sqrt 0"; |
26 val SOME (t',_) = rewrite_set_ ctxt false Root_erls t; |
26 val SOME (t',_) = rewrite_set_ ctxt false Root_erls t; |
27 if UnparseC.term t' = "0" then () else error "root.sml: diff.behav. sqrt 1"; |
27 if UnparseC.term t' = "0" then () else error "root.sml: diff.behav. sqrt 1"; |
28 |
28 |