src/ZF/simpdata.ML
changeset 485 5e00a676a211
parent 467 92868dab2939
child 516 1957113f0d7d
     1.1 --- a/src/ZF/simpdata.ML	Tue Jul 26 13:21:20 1994 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Tue Jul 26 13:44:42 1994 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4  
     1.5  val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
     1.6  		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
     1.7 -		triv_RepFun];
     1.8 +		triv_RepFun, subset_refl];
     1.9  
    1.10  (*Sigma_cong, Pi_cong NOT included by default since they cause
    1.11    flex-flex pairs and the "Check your prover" error -- because most