equal
deleted
inserted
replaced
30 collections algebra_simps or field_simps to obtain reasonable |
30 collections algebra_simps or field_simps to obtain reasonable |
31 simplification. INCOMPATIBILITY. |
31 simplification. INCOMPATIBILITY. |
32 |
32 |
33 * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) |
33 * Theory HOL-Library.Monad_Syntax: infix operation "bind" (>>=) |
34 associates to the left now as is customary. |
34 associates to the left now as is customary. |
|
35 |
|
36 |
|
37 *** ML *** |
|
38 |
|
39 * Theory construction may be forked internally, the operation |
|
40 Theory.join_theory recovers a single result theory. See also the example |
|
41 in theory "HOL-ex.Join_Theory". |
35 |
42 |
36 |
43 |
37 |
44 |
38 New in Isabelle2019 (June 2019) |
45 New in Isabelle2019 (June 2019) |
39 ------------------------------- |
46 ------------------------------- |