src/ZF/simpdata.ML
changeset 516 1957113f0d7d
parent 485 5e00a676a211
child 533 7357160bc56a
     1.1 --- a/src/ZF/simpdata.ML	Fri Aug 12 12:28:46 1994 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Fri Aug 12 12:51:34 1994 +0200
     1.3 @@ -50,9 +50,8 @@
     1.4  
     1.5  val ZF_typechecks = [if_type,lam_type,SigmaI,apply_type,split_type];
     1.6  
     1.7 -(*To instantiate variables in typing conditions; 
     1.8 -  to perform type checking faster than rewriting can
     1.9 -  NOT TERRIBLY USEFUL because it does not simplify conjunctions*)
    1.10 +(*Instantiates variables in typing conditions.
    1.11 +  drawback: does not simplify conjunctions*)
    1.12  fun type_auto_tac tyrls hyps = SELECT_GOAL
    1.13      (DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
    1.14             ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));