src/Tools/isac/Specify/Specify.thy
changeset 60776 c2e6848d3dce
parent 60775 c31ae770d74c
child 60782 e797d1bdfe37
     1.1 --- a/src/Tools/isac/Specify/Specify.thy	Thu Dec 07 17:16:22 2023 +0100
     1.2 +++ b/src/Tools/isac/Specify/Specify.thy	Sun Dec 10 07:56:02 2023 +0100
     1.3 @@ -26,7 +26,18 @@
     1.4  
     1.5  ML \<open>
     1.6  \<close> ML \<open>
     1.7 -
     1.8 +\<close> ML \<open>
     1.9 +\<close> ML \<open>
    1.10 +\<close> ML \<open>
    1.11 +\<close> ML \<open>
    1.12 +\<close> ML \<open>
    1.13 +\<close> ML \<open>
    1.14 +\<close> ML \<open>
    1.15 +I_Model.is_error: I_Model.feedback_POS -> bool
    1.16 +\<close> ML \<open>
    1.17 +P_Model.mk_delete: theory -> string -> I_Model.feedback_POS -> Tactic.input
    1.18 +\<close> ML \<open>
    1.19 +P_Model.mk_additem: string -> TermC.as_string -> Tactic.input
    1.20  \<close> ML \<open>
    1.21  \<close>
    1.22  end