src/ZF/simpdata.ML
changeset 435 ca5356bd315a
parent 279 7738aed3f84d
child 467 92868dab2939
equal deleted inserted replaced
434:89d45187f04d 435:ca5356bd315a
    77 	      Const(a,_) => 
    77 	      Const(a,_) => 
    78 		(case assoc(pairs,a) of
    78 		(case assoc(pairs,a) of
    79 		     Some rls => flat (map atomize ([th] RL rls))
    79 		     Some rls => flat (map atomize ([th] RL rls))
    80 		   | None     => [th])
    80 		   | None     => [th])
    81 	    | _ => [th]
    81 	    | _ => [th]
    82   in case concl_of th of (*The operator below is Trueprop*)
    82   in case concl_of th of 
    83 	_ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b
    83        Const("Trueprop",_) $ P => 
    84       | _ $ (Const("True",_)) => []	(*True is DELETED*)
    84 	  (case P of
    85       | _ $ (Const("False",_)) => []	(*should False do something??*)
    85 	       Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b
    86       | _ $ A => tryrules atomize_pairs A
    86 	     | Const("True",_)         => []
       
    87 	     | Const("False",_)        => []
       
    88 	     | A => tryrules atomize_pairs A)
       
    89      | _                       => [th]
    87   end;
    90   end;
    88 
    91 
    89 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
    92 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
    90 		beta, eta, restrict, fst_conv, snd_conv, split];
    93 		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff];
    91 
    94 
    92 (*Sigma_cong, Pi_cong NOT included by default since they cause
    95 (*Sigma_cong, Pi_cong NOT included by default since they cause
    93   flex-flex pairs and the "Check your prover" error -- because most
    96   flex-flex pairs and the "Check your prover" error -- because most
    94   Sigma's and Pi's are abbreviated as * or -> *)
    97   Sigma's and Pi's are abbreviated as * or -> *)
    95 val ZF_congs =
    98 val ZF_congs =