equal
deleted
inserted
replaced
5 (quotient_term.ML) |
5 (quotient_term.ML) |
6 |
6 |
7 |
7 |
8 Higher Priority |
8 Higher Priority |
9 =============== |
9 =============== |
|
10 |
|
11 |
|
12 - Also, in the interest of making nicer generated documentation, you |
|
13 might want to change all your "section" headings in Quotient.thy to |
|
14 "subsection", and add a "header" statement to the top of the file. |
|
15 Otherwise, each "section" gets its own chapter in the generated pdf, |
|
16 when the rest of HOL has one chapter per theory file (the chapter |
|
17 title comes from the "header" statement). |
10 |
18 |
11 - If the constant definition gives the wrong definition |
19 - If the constant definition gives the wrong definition |
12 term, one gets a cryptic message about absrep_fun |
20 term, one gets a cryptic message about absrep_fun |
13 |
21 |
14 - Handle theorems that include Ball/Bex. For this, would |
22 - Handle theorems that include Ball/Bex. For this, would |