src/ZF/simpdata.ML
changeset 516 1957113f0d7d
parent 485 5e00a676a211
child 533 7357160bc56a
equal deleted inserted replaced
515:abcc438e7c27 516:1957113f0d7d
    48 
    48 
    49 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
    49 fun typechk_tac tyrls = REPEAT (typechk_step_tac tyrls);
    50 
    50 
    51 val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
    51 val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
    52 
    52 
    53 (*To instantiate variables in typing conditions; 
    53 (*Instantiates variables in typing conditions.
    54   to perform type checking faster than rewriting can
    54   drawback: does not simplify conjunctions*)
    55   NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
       
    56 fun type_auto_tac tyrls hyps = SELECT_GOAL
    55 fun type_auto_tac tyrls hyps = SELECT_GOAL
    57     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    56     (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    58            ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
    57            ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
    59 
    58 
    60 (** New version of mk_rew_rules **)
    59 (** New version of mk_rew_rules **)