1.1 --- a/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy Fri Apr 10 18:32:36 2020 +0200
1.3 @@ -12,7 +12,7 @@
1.4 @{term "\<delta> "};
1.5 @{term "\<phi> "};
1.6 @{term "\<rho> "};
1.7 - UnparseC.term2str @{term "\<rho> "};
1.8 + UnparseC.term @{term "\<rho> "};
1.9 \<close>
1.10
1.11 section\<open>Working with Rulesets\<close>
1.12 @@ -48,9 +48,9 @@
1.13 \<close>
1.14
1.15 ML\<open>
1.16 - UnparseC.term2str t';
1.17 - UnparseC.term2str t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.18 - UnparseC.term2str t' = "?u [?n] + \<alpha>^^^?n u[n] + ?\<delta> [?n]";
1.19 + UnparseC.term t';
1.20 + UnparseC.term t' = "z / (z - ?\<delta> [?n]) + z / (z - \<alpha>) + ?\<delta> [?n]";
1.21 + UnparseC.term t' = "?u [?n] + \<alpha>^^^?n u[n] + ?\<delta> [?n]";
1.22 \<close>
1.23
1.24 text\<open>Problems: Rule~1 is applied before the expression is checked for Rule~4