equal
deleted
inserted
replaced
6 |
6 |
7 New in this Isabelle version |
7 New in this Isabelle version |
8 ---------------------------- |
8 ---------------------------- |
9 |
9 |
10 *** General *** |
10 *** General *** |
|
11 |
|
12 * Embedded content (e.g. the inner syntax of types, terms, props) may be |
|
13 delimited uniformly via cartouches. This works better than old-fashioned |
|
14 quotes when sub-languages are nested. |
11 |
15 |
12 * Type-inference improves sorts of newly introduced type variables for |
16 * Type-inference improves sorts of newly introduced type variables for |
13 the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL). |
17 the object-logic, using its base sort (i.e. HOL.type for Isabelle/HOL). |
14 Thus terms like "f x" or "\<And>x. P x" without any further syntactic context |
18 Thus terms like "f x" or "\<And>x. P x" without any further syntactic context |
15 produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare |
19 produce x::'a::type in HOL instead of x::'a::{} in Pure. Rare |