removed True_implies (cf. True_implies_equals);
authorwenzelm
Thu Aug 03 15:03:07 2006 +0200 (2006-08-03)
changeset 20320a5368278a72c
parent 20319 a8761e8568de
child 20321 b7c0bf788f50
removed True_implies (cf. True_implies_equals);
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Aug 03 15:03:05 2006 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Aug 03 15:03:07 2006 +0200
     1.3 @@ -25,8 +25,6 @@
     1.4  
     1.5  open FundefCommon
     1.6  
     1.7 -val True_implies = thm "True_implies"
     1.8 -
     1.9  
    1.10  fun add_simps label moreatts (MutualPart {f_name, ...}, psimps) spec_part thy =
    1.11      let 
    1.12 @@ -112,7 +110,7 @@
    1.13  	val (FundefMResult {psimps, simple_pinducts, ... }, Mutual {parts, ...}, spec)
    1.14  	  = the (get_fundef_data name thy)
    1.15  
    1.16 -	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies])
    1.17 +	val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    1.18  
    1.19  	val tsimps = map (map remove_domain_condition) psimps
    1.20  	val tinduct = map remove_domain_condition simple_pinducts