summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

adapted proofs to slightly changed definitions of congruent(2)

reorienting iff in Quotient_rel prevents simplifier looping;
lemma QuotientI;
tuned theory text

replaced slightly odd locale congruent2 by plain definition

replaced slightly odd locale congruent by plain definition

equivI has replaced equiv.intro

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
moved generic definitions about relations from Quotient.thy to Predicate;
consistent use of R rather than E for relations;
more natural deduction rules

moved generic definitions about relations from Quotient.thy to Predicate;
more natural deduction rules

moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
more natural deduction rules;
replaced slightly odd locale equiv by plain definition

simplify proof of LIMSEQ_unique

use new 'file' antiquotation for reference to Dedekind_Real.thy