src/HOL/simpdata.ML
changeset 4744 4469d498cd48
parent 4743 b3bfcbd9fb93
child 4769 bb60149fe21b
equal deleted inserted replaced
4743:b3bfcbd9fb93 4744:4469d498cd48
   398 
   398 
   399 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
   399 val HOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
   400 			    setSSolver   safe_solver
   400 			    setSSolver   safe_solver
   401 			    setSolver  unsafe_solver
   401 			    setSolver  unsafe_solver
   402 			    setmksimps (mksimps mksimps_pairs)
   402 			    setmksimps (mksimps mksimps_pairs)
   403 			    setmkeqTrue mk_meta_eq_True
   403 			    setmkeqTrue mk_meta_eq_True;
   404                             addsplits [expand_if];
       
   405 
   404 
   406 val HOL_ss = 
   405 val HOL_ss = 
   407     HOL_basic_ss addsimps 
   406     HOL_basic_ss addsimps 
   408      ([triv_forall_equality, (* prunes params *)
   407      ([triv_forall_equality, (* prunes params *)
   409        True_implies_equals, (* prune asms `True' *)
   408        True_implies_equals, (* prune asms `True' *)
   411        o_apply, imp_disjL, conj_assoc, disj_assoc,
   410        o_apply, imp_disjL, conj_assoc, disj_assoc,
   412        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
   411        de_Morgan_conj, de_Morgan_disj, imp_disj1, imp_disj2, not_imp,
   413        disj_not1, not_all, not_ex, cases_simp]
   412        disj_not1, not_all, not_ex, cases_simp]
   414      @ ex_simps @ all_simps @ simp_thms)
   413      @ ex_simps @ all_simps @ simp_thms)
   415      addsimprocs [defALL_regroup,defEX_regroup]
   414      addsimprocs [defALL_regroup,defEX_regroup]
   416      addcongs [imp_cong];
   415      addcongs [imp_cong]
       
   416      addsplits [expand_if];
   417 
   417 
   418 qed_goal "if_distrib" HOL.thy
   418 qed_goal "if_distrib" HOL.thy
   419   "f(if c then x else y) = (if c then f x else f y)" 
   419   "f(if c then x else y) = (if c then f x else f y)" 
   420   (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
   420   (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
   421 
   421