remove needless Metis facts
authorblanchet
Tue Oct 05 12:04:57 2010 +0200 (2010-10-05)
changeset 39956132b79985660
parent 39955 cb9cac7eba29
child 39957 2f2d90cc31a2
remove needless Metis facts
src/HOL/Quotient.thy
     1.1 --- a/src/HOL/Quotient.thy	Tue Oct 05 12:04:49 2010 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Tue Oct 05 12:04:57 2010 +0200
     1.3 @@ -319,12 +319,12 @@
     1.4  lemma ball_reg_right:
     1.5    assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
     1.6    shows "All P \<longrightarrow> Ball R Q"
     1.7 -  using a by (metis COMBC_def Collect_def Collect_mem_eq)
     1.8 +  using a by (metis Collect_def Collect_mem_eq)
     1.9  
    1.10  lemma bex_reg_left:
    1.11    assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
    1.12    shows "Bex R Q \<longrightarrow> Ex P"
    1.13 -  using a by (metis COMBC_def Collect_def Collect_mem_eq)
    1.14 +  using a by (metis Collect_def Collect_mem_eq)
    1.15  
    1.16  lemma ball_reg_left:
    1.17    assumes a: "equivp R"
    1.18 @@ -381,13 +381,13 @@
    1.19    assumes a: "!x :: 'a. (R x --> P x --> Q x)"
    1.20    and     b: "Ball R P"
    1.21    shows "Ball R Q"
    1.22 -  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
    1.23 +  using a b by (metis Collect_def Collect_mem_eq)
    1.24  
    1.25  lemma bex_reg:
    1.26    assumes a: "!x :: 'a. (R x --> P x --> Q x)"
    1.27    and     b: "Bex R P"
    1.28    shows "Bex R Q"
    1.29 -  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
    1.30 +  using a b by (metis Collect_def Collect_mem_eq)
    1.31  
    1.32  
    1.33  lemma ball_all_comm: