declare 'defn' rules;
authorwenzelm
Sun Jan 29 19:23:38 2006 +0100 (2006-01-29)
changeset 188326ab4de872a70
parent 18831 f1315d118059
child 18833 bead1a4e966b
declare 'defn' rules;
src/HOL/HOL.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Sat Jan 28 17:29:49 2006 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sun Jan 29 19:23:38 2006 +0100
     1.3 @@ -904,6 +904,7 @@
     1.4  qed
     1.5  
     1.6  lemmas [symmetric, rulify] = atomize_all atomize_imp
     1.7 +  and [symmetric, defn] = atomize_all atomize_imp atomize_eq
     1.8  
     1.9  
    1.10  subsubsection {* Classical Reasoner setup *}
     2.1 --- a/src/HOL/Set.thy	Sat Jan 28 17:29:49 2006 +0100
     2.2 +++ b/src/HOL/Set.thy	Sun Jan 29 19:23:38 2006 +0100
     2.3 @@ -1011,7 +1011,8 @@
     2.4      "(!!x. x \<in> A ==> P x) == Trueprop (\<forall>x\<in>A. P x)"
     2.5    by (simp only: Ball_def atomize_all atomize_imp)
     2.6  
     2.7 -declare atomize_ball [symmetric, rulify]
     2.8 +lemmas [symmetric, rulify] = atomize_ball
     2.9 +  and [symmetric, defn] = atomize_ball
    2.10  
    2.11  
    2.12  subsection {* Further set-theory lemmas *}