1.1 --- a/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Sep 05 18:09:56 2018 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Inverse_Z_Transform.thy	Wed Nov 21 12:32:54 2018 +0100
     1.3 @@ -20,13 +20,13 @@
     1.4    ruleZY: "(X z = a / b) = (X' z = a / (z * b))" and
     1.5    ruleYZ: "(a/b + c/d) = (a*(z/b) + c*(z/d))" 
     1.6  
     1.7 -subsection{*Define the Field Descriptions for the specification*}
     1.8 +subsection\<open>Define the Field Descriptions for the specification\<close>
     1.9  consts
    1.10    filterExpression  :: "bool => una"
    1.11    stepResponse      :: "bool => una"
    1.12  
    1.13  
    1.14 -ML {*
    1.15 +ML \<open>
    1.16  val inverse_z = prep_rls'(
    1.17    Rule.Rls {id = "inverse_z", preconds = [], rew_ord = ("dummy_ord",Rule.dummy_ord), 
    1.18  	  erls = Rule.Erls, srls = Rule.Erls, calc = [], errpatts = [],
    1.19 @@ -35,18 +35,18 @@
    1.20      Rule.Thm ("rule4", @{thm rule4})
    1.21  	   ], 
    1.22  	 scr = Rule.EmptyScr});
    1.23 -*}
    1.24 +\<close>
    1.25  
    1.26  
    1.27 -text {*store the rule set for math engine*}
    1.28 +text \<open>store the rule set for math engine\<close>
    1.29  
    1.30 -setup {* KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))] *}
    1.31 +setup \<open>KEStore_Elems.add_rlss [("inverse_z", (Context.theory_name @{theory}, inverse_z))]\<close>
    1.32  
    1.33 -subsection{*Define the Specification*}
    1.34 -ML {*
    1.35 +subsection\<open>Define the Specification\<close>
    1.36 +ML \<open>
    1.37  val thy = @{theory};
    1.38 -*}
    1.39 -setup {* KEStore_Elems.add_pbts
    1.40 +\<close>
    1.41 +setup \<open>KEStore_Elems.add_pbts
    1.42    [(Specify.prep_pbt thy "pbl_SP" [] Celem.e_pblID (["SignalProcessing"], [], Rule.e_rls, NONE, [])),
    1.43      (Specify.prep_pbt thy "pbl_SP_Ztrans" [] Celem.e_pblID
    1.44        (["Z_Transform","SignalProcessing"], [], Rule.e_rls, NONE, [])),
    1.45 @@ -63,16 +63,16 @@
    1.46          [("#Given" ,["filterExpression X_eq"]),
    1.47            ("#Find"  ,["stepResponse n_eq"])],
    1.48          Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)], NONE, 
    1.49 -        [["SignalProcessing","Z_Transform","Inverse"]]))] *}
    1.50 +        [["SignalProcessing","Z_Transform","Inverse"]]))]\<close>
    1.51  
    1.52 -subsection {*Define Name and Signature for the Method*}
    1.53 +subsection \<open>Define Name and Signature for the Method\<close>
    1.54  consts
    1.55    InverseZTransform :: "[bool, bool] => bool"
    1.56      ("((Script InverseZTransform (_ =))// (_))" 9)
    1.57  
    1.58 -subsection {*Setup Parent Nodes in Hierarchy of Method*}
    1.59 -ML {* val thy = @{theory}; (*latest version of thy required*) *}
    1.60 -setup {* KEStore_Elems.add_mets
    1.61 +subsection \<open>Setup Parent Nodes in Hierarchy of Method\<close>
    1.62 +ML \<open>val thy = @{theory}; (*latest version of thy required*)\<close>
    1.63 +setup \<open>KEStore_Elems.add_mets
    1.64    [Specify.prep_met thy "met_SP" [] Celem.e_metID
    1.65        (["SignalProcessing"], [],
    1.66          {rew_ord'="tless_true", rls'= Rule.e_rls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls, crls = Rule.e_rls,
    1.67 @@ -234,7 +234,7 @@
    1.68            "  n_eq = drop_questionmarks n_eq                   "^
    1.69            (*([], Res), X_z = 4 * (1 / 2) ^^^ n * u [n] + -4 * (-1 / 4) ^^^ n * u [n]*)
    1.70            "in n_eq)")]
    1.71 -*}
    1.72 +\<close>
    1.73  
    1.74  end
    1.75