1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Jun 10 11:54:20 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Thu Jun 10 12:23:57 2021 +0200
     1.3 @@ -46,10 +46,10 @@
     1.4  val thy = @{theory};
     1.5  \<close>
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Problem.prep_input thy "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
     1.8 -    (Problem.prep_input thy "pbl_SP_Ztrans" [] Problem.id_empty
     1.9 +  [(Problem.prep_input @{theory} "pbl_SP" [] Problem.id_empty (["SignalProcessing"], [], Rule_Set.empty, NONE, [])),
    1.10 +    (Problem.prep_input @{theory} "pbl_SP_Ztrans" [] Problem.id_empty
    1.11        (["Z_Transform", "SignalProcessing"], [], Rule_Set.empty, NONE, [])),
    1.12 -    (Problem.prep_input thy "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.13 +    (Problem.prep_input @{theory} "pbl_SP_Ztrans_inv" [] Problem.id_empty
    1.14        (["Inverse", "Z_Transform", "SignalProcessing"],
    1.15          [("#Given" , ["filterExpression X_eq"]),
    1.16            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.17 @@ -57,13 +57,13 @@
    1.18          [["SignalProcessing", "Z_Transform", "Inverse"]]))]\<close>
    1.19  
    1.20  subsection \<open>Setup Parent Nodes in Hierarchy of MethodC\<close>
    1.21 -ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
    1.22 +
    1.23  setup \<open>KEStore_Elems.add_mets
    1.24 -    [MethodC.prep_input thy "met_SP" [] MethodC.id_empty
    1.25 +    [MethodC.prep_input @{theory} "met_SP" [] MethodC.id_empty
    1.26        (["SignalProcessing"], [],
    1.27          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.28            errpats = [], nrls = Rule_Set.empty}, @{thm refl}),
    1.29 -    MethodC.prep_input thy "met_SP_Ztrans" [] MethodC.id_empty
    1.30 +    MethodC.prep_input @{theory} "met_SP_Ztrans" [] MethodC.id_empty
    1.31        (["SignalProcessing", "Z_Transform"], [],
    1.32          {rew_ord'="tless_true", rls'= Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty, crls = Rule_Set.empty,
    1.33            errpats = [], nrls = Rule_Set.empty}, @{thm refl})]
    1.34 @@ -87,7 +87,7 @@
    1.35          [BOOL equ, REAL X_z]
    1.36    in X) "
    1.37  setup \<open>KEStore_Elems.add_mets
    1.38 -    [MethodC.prep_input thy "met_SP_Ztrans_inv" [] MethodC.id_empty
    1.39 +    [MethodC.prep_input @{theory} "met_SP_Ztrans_inv" [] MethodC.id_empty
    1.40        (["SignalProcessing", "Z_Transform", "Inverse"],
    1.41          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.42            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>
    1.43 @@ -115,7 +115,7 @@
    1.44      n_eq = (Rewrite_Set ''inverse_z'' ) X_zeq
    1.45    in n_eq)"
    1.46  setup \<open>KEStore_Elems.add_mets
    1.47 -    [MethodC.prep_input thy "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
    1.48 +    [MethodC.prep_input @{theory} "met_SP_Ztrans_inv_sub" [] MethodC.id_empty
    1.49        (["SignalProcessing", "Z_Transform", "Inverse_sub"],
    1.50          [("#Given" ,["filterExpression X_eq", "functionName X_z"]),
    1.51            ("#Find"  ,["stepResponse n_eq"])], \<comment> \<open>TODO: unused, "u [n]" is introduced by rule1..6\<close>