src/HOL/Old_Number_Theory/EulerFermat.thy
changeset 45605 a89b4bc311a5
parent 45480 a39bb6d42ace
child 46008 c296c75f4cf4
     1.1 --- a/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 20 20:59:30 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/EulerFermat.thy	Sun Nov 20 21:05:23 2011 +0100
     1.3 @@ -196,10 +196,8 @@
     1.4    apply (rule aux_some, simp_all)
     1.5    done
     1.6  
     1.7 -lemmas RRset2norRR_correct1 =
     1.8 -  RRset2norRR_correct [THEN conjunct1, standard]
     1.9 -lemmas RRset2norRR_correct2 =
    1.10 -  RRset2norRR_correct [THEN conjunct2, standard]
    1.11 +lemmas RRset2norRR_correct1 = RRset2norRR_correct [THEN conjunct1]
    1.12 +lemmas RRset2norRR_correct2 = RRset2norRR_correct [THEN conjunct2]
    1.13  
    1.14  lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
    1.15    by (induct set: RsetR) auto