equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "Quotient" |
3 imports "Quotient" |
4 "LaTeXsugar" |
4 "LaTeXsugar" |
5 begin |
5 begin |
6 |
6 |
7 notation (latex output) |
7 notation (latex output) |
8 rel_conj ("_ OOO _" [53, 53] 52) |
8 rel_conj ("_ OOO _" [53, 53] 52) |
73 In the context of HOL, there have been several quotient packages (...). The |
73 In the context of HOL, there have been several quotient packages (...). The |
74 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
74 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
75 surprising, none of them can deal compositions of quotients, for example with |
75 surprising, none of them can deal compositions of quotients, for example with |
76 lifting theorems about @{text "concat"}: |
76 lifting theorems about @{text "concat"}: |
77 |
77 |
78 @{text [display] "concat definition"} |
78 @{thm concat.simps(1)}\\ |
79 |
79 @{thm concat.simps(2)[no_vars]} |
|
80 |
80 \noindent |
81 \noindent |
81 One would like to lift this definition to the operation |
82 One would like to lift this definition to the operation |
82 |
83 |
83 @{text [display] "union definition"} |
84 @{text [display] "union definition"} |
84 |
85 |