Walther@60764: (* Title:  "Specify/Specify.thy"
wneuper@59594:    Author: Walther Neuper 110226
wneuper@59594:    (c) due to copyright terms
Walther@60764: 
Walther@60764:  Specification phase
wneuper@59594:  *)
wneuper@59594: 
wneuper@59594: theory Specify
wenzelm@60314:   imports "$ISABELLE_ISAC/MathEngBasic/MathEngBasic"
wenzelm@60314:   keywords "cas" :: thy_decl
wneuper@59594: begin
walther@59938:   ML_file "o-model.sml"
Walther@60705:   ML_file "pre-conditions.sml" (*uses Model_Def.i_model*)
walther@59938:   ML_file "i-model.sml"
walther@59959:   ML_file "p-model.sml"
walther@59984:   ML_file "m-match.sml"
walther@59960:   ML_file refine.sml
walther@59959:   ML_file "test-out.sml"
walther@59933:   ML_file "specify-step.sml"
walther@59981:   ML_file specification.sml
walther@59982:   ML_file "cas-command.sml"
walther@59984:   ML_file "p-spec.sml"
Walther@60772:   ML_file specify.sml                                            
Walther@60609:   ML_file "sub-problem.sml"
walther@59764:   ML_file "step-specify.sml"
wneuper@59595: 
wneuper@59594: ML \<open>
walther@60009: \<close> ML \<open>
Walther@60776: \<close> ML \<open>
Walther@60776: \<close> ML \<open>
Walther@60776: \<close> ML \<open>
Walther@60776: \<close> ML \<open>
Walther@60776: \<close> ML \<open>
Walther@60776: \<close> ML \<open>
Walther@60776: \<close> ML \<open>
Walther@60782: I_Model.is_error: I_Model.feedback -> bool
Walther@60776: \<close> ML \<open>
Walther@60782: P_Model.mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
Walther@60776: \<close> ML \<open>
Walther@60776: P_Model.mk_additem: string -> TermC.as_string -> Tactic.input
wneuper@59594: \<close> ML \<open>
wneuper@59594: \<close>
wneuper@59594: end