equal
deleted
inserted
replaced
15 * Antiquotations @{scala}, @{scala_object}, @{scala_type}, |
15 * Antiquotations @{scala}, @{scala_object}, @{scala_type}, |
16 @{scala_method} refer to checked Isabelle/Scala entities. |
16 @{scala_method} refer to checked Isabelle/Scala entities. |
17 |
17 |
18 |
18 |
19 *** Pure *** |
19 *** Pure *** |
|
20 |
|
21 * Session Pure-Examples contains notable examples for Isabelle/Pure |
|
22 (former entries of HOL-Isar_Examples). |
20 |
23 |
21 * Definitions in locales produce rule which can be added as congruence |
24 * Definitions in locales produce rule which can be added as congruence |
22 rule to protect foundational terms during simplification. |
25 rule to protect foundational terms during simplification. |
23 |
26 |
24 |
27 |