equal
deleted
inserted
replaced
28 * Instantiation target allows for simultaneous specification of class |
28 * Instantiation target allows for simultaneous specification of class |
29 instance operations together with an instantiation proof. |
29 instance operations together with an instantiation proof. |
30 Type-checking phase allows to refer to class operations uniformly. |
30 Type-checking phase allows to refer to class operations uniformly. |
31 See HOL/Complex/Complex.thy for an Isar example and |
31 See HOL/Complex/Complex.thy for an Isar example and |
32 HOL/Library/Eval.thy for an ML example. |
32 HOL/Library/Eval.thy for an ML example. |
|
33 |
|
34 * Indexing of literal facts: be more serious about including only |
|
35 facts from the visible specification/proof context, but not the |
|
36 background context (locale etc.). Affects `prop` notation and method |
|
37 "fact". INCOMPATIBILITY: need to name facts explicitly in rare |
|
38 situations. |
33 |
39 |
34 |
40 |
35 *** HOL *** |
41 *** HOL *** |
36 |
42 |
37 * Library/RBT.thy: New theory of red-black trees, an efficient |
43 * Library/RBT.thy: New theory of red-black trees, an efficient |