equal
deleted
inserted
replaced
41 \<close> |
41 \<close> |
42 |
42 |
43 text\<open>Apply the Ruleset to a term\<close> |
43 text\<open>Apply the Ruleset to a term\<close> |
44 |
44 |
45 ML \<open> |
45 ML \<open> |
46 val t = str2term "z / (z - 1) + z / (z - \<alpha>) + 1::real"; |
46 val t = parse_test @{context} "z / (z - 1) + z / (z - \<alpha>) + 1::real"; |
47 val SOME (t', asm) = rewrite_set_ thy true transform t; |
47 val SOME (t', asm) = rewrite_set_ thy true transform t; |
48 \<close> |
48 \<close> |
49 |
49 |
50 ML\<open> |
50 ML\<open> |
51 UnparseC.term t'; |
51 UnparseC.term t'; |