equal
deleted
inserted
replaced
19 val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term |
19 val eval: Proof.context -> Rule_Set.T -> bool * term -> bool * term |
20 |
20 |
21 val max_variant: Model_Def.i_model -> Model_Def.variant |
21 val max_variant: Model_Def.i_model -> Model_Def.variant |
22 val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T |
22 val environment_TEST: Model_Pattern.T -> Model_Def.i_model_TEST -> Env.T |
23 |
23 |
|
24 (*TODO: replace in pre-conditions.m, see fun max_variants + make_envs_preconds, |
|
25 see i-model.sml (** complete I_Model.T **) *) |
24 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST -> |
26 val of_max_variant: Model_Pattern.T -> Model_Def.i_model_TEST -> |
25 (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval) |
27 (bool * Model_Def.variant * Model_Def.i_model_TEST) * Env.T * (env_subst * env_eval) |
26 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> |
28 val make_envs_preconds: (Model_Pattern.single * Model_Def.i_model_single_TEST) list -> |
27 ((term * term) * (term * term)) list |
29 ((term * term) * (term * term)) list |
28 |
30 |