equal
deleted
inserted
replaced
10 val ct = "sort [1,4,3,2]"; |
10 val ct = "sort [1,4,3,2]"; |
11 "--- 1 ---"; |
11 "--- 1 ---"; |
12 val rls = "ins_sort"; |
12 val rls = "ins_sort"; |
13 val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct); |
13 val (ct,_) = the (rewrite_set thy' "eval_rls" false rls ct); |
14 if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK" |
14 if ct="[1, 2, 3, 4]" then "sort [1,4,3,2] OK" |
15 else raise error "sort [1,4,3,2] didn't work"; |
15 else error "sort [1,4,3,2] didn't work"; |
16 |
16 |
17 |
17 |
18 "---------------- sort [1,3,2] by rewrite stepwise ----------------"; |
18 "---------------- sort [1,3,2] by rewrite stepwise ----------------"; |
19 val thy' = "InsSort"; |
19 val thy' = "InsSort"; |
20 val ct = "sort [1,3,2]"; |
20 val ct = "sort [1,3,2]"; |
81 "--- 16 ---"; |
81 "--- 16 ---"; |
82 val thm = ("foldr_base",""); |
82 val thm = ("foldr_base",""); |
83 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
83 val (ct,_) = the (rewrite thy' "tless_true" "eval_rls" false thm ct); |
84 (*val ct = "[#1, #2, #3]"*) |
84 (*val ct = "[#1, #2, #3]"*) |
85 if ct="[1, 2, 3]" then "sort [1,3,2] OK" |
85 if ct="[1, 2, 3]" then "sort [1,3,2] OK" |
86 else raise error "sort [1,3,2] didn't work"; |
86 else error "sort [1,3,2] didn't work"; |
87 |
87 |
88 |
88 |
89 "---------------- sort [1,3,2] from script ----------------"; |
89 "---------------- sort [1,3,2] from script ----------------"; |
90 val fmz = ["unsorted [1,3,2]", "sorted S"]; |
90 val fmz = ["unsorted [1,3,2]", "sorted S"]; |
91 val (dI',pI',mI') = |
91 val (dI',pI',mI') = |