1.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Nov 29 18:09:44 2018 +0100
1.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Nov 30 12:27:18 2018 +0100
1.3 @@ -463,7 +463,7 @@
1.4
1.5 text\<open>\noindent First we isolate the difficulty in the program as follows:
1.6 \begin{verbatim}
1.7 - " (L_L::bool list) = (SubProblem (PolyEq', " ^
1.8 + " (L_L::bool list) = (SubProblem (PolyEqX, " ^
1.9 " [abcFormula, degree_2, polynomial, " ^
1.10 " univariate,equation], " ^
1.11 " [no_met]) " ^
1.12 @@ -1024,7 +1024,7 @@
1.13 (*
1.14 * simplify
1.15 *)
1.16 - " X' = (SubProblem (Isac',[pqFormula,degree_2, "^
1.17 + " X' = (SubProblem (IsacX,[pqFormula,degree_2, "^
1.18 " polynomial,univariate,equation], "^
1.19 " [no_met]) "^
1.20 " [BOOL e_e, REAL v_v]) "^
1.21 @@ -1067,7 +1067,7 @@
1.22 *)
1.23 " (equ::bool) = (denom = (0::real)); "^
1.24 " (L_L::bool list) = "^
1.25 - " (SubProblem (Test', "^
1.26 + " (SubProblem (TestX, "^
1.27 " [LINEAR,univariate,equation,test], "^
1.28 " [Test,solve_linear]) "^
1.29 " [BOOL equ, REAL z]) "^
1.30 @@ -1147,7 +1147,7 @@
1.31 " (num::real) = get_numerator funterm; "^
1.32 (*get_numerator*)
1.33 " (equ::bool) = (denom = (0::real)); "^
1.34 - " (L_L::bool list) = (SubProblem (PolyEq', "^
1.35 + " (L_L::bool list) = (SubProblem (PolyEqX, "^
1.36 " [abcFormula,degree_2,polynomial,univariate,equation], "^
1.37 " [no_met]) "^
1.38 " [BOOL equ, REAL zzz]); "^
1.39 @@ -1172,7 +1172,7 @@
1.40 " eq_a = (Substitute [zzz=z1]) eq; "^
1.41 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
1.42 " (sol_a::bool list) = "^
1.43 - " (SubProblem (Isac', "^
1.44 + " (SubProblem (IsacX, "^
1.45 " [univariate,equation],[no_met]) "^
1.46 " [BOOL eq_a, REAL (A::real)]); "^
1.47 " (a::real) = (rhs(NTH 1 sol_a)); "^
1.48 @@ -1181,7 +1181,7 @@
1.49 " eq_b = (Substitute [zzz=z2]) eq_b; "^
1.50 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
1.51 " (sol_b::bool list) = "^
1.52 - " (SubProblem (Isac', "^
1.53 + " (SubProblem (IsacX, "^
1.54 " [univariate,equation],[no_met]) "^
1.55 " [BOOL eq_b, REAL (B::real)]); "^
1.56 " (b::real) = (rhs(NTH 1 sol_b)); "^