the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"

     1

(*<*)

     2

theory Paper

     3

imports "../Quot/QuotMain"

     4

begin

     5

(*>*)

     6

     7

section {* Introduction *}

     8

     9

text {*

    10

  Here can come any text.

    11

    12

*}

    13

    14

(*<*)

    15

end

    16

(*>*)