test/Tools/isac/ADDTESTS/course/CADGME/example_2.thy
changeset 59868 d77aa0992e0f
parent 59861 65ec9f679c3f
child 59871 82428ca0d23e
     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