equal
deleted
inserted
replaced
59 |
59 |
60 See src/HOL/ex/Computations.thy, |
60 See src/HOL/ex/Computations.thy, |
61 src/HOL/Decision_Procs/Commutative_Ring.thy and |
61 src/HOL/Decision_Procs/Commutative_Ring.thy and |
62 src/HOL/Decision_Procs/Reflective_Field.thy for examples and the |
62 src/HOL/Decision_Procs/Reflective_Field.thy for examples and the |
63 tutorial on code generation. |
63 tutorial on code generation. |
|
64 |
|
65 * Commands 'alias' and 'type_alias' introduce aliases for constants and |
|
66 type constructors, respectively. This allows adhoc changes to name-space |
|
67 accesses within global or local theory contexts, e.g. within a 'bundle'. |
64 |
68 |
65 |
69 |
66 *** Prover IDE -- Isabelle/Scala/jEdit *** |
70 *** Prover IDE -- Isabelle/Scala/jEdit *** |
67 |
71 |
68 * Automatic indentation is more careful to avoid redundant spaces in |
72 * Automatic indentation is more careful to avoid redundant spaces in |