equal
deleted
inserted
replaced
42 bundle foo |
42 bundle foo |
43 begin |
43 begin |
44 declare a [simp] |
44 declare a [simp] |
45 declare b [intro] |
45 declare b [intro] |
46 end |
46 end |
|
47 |
|
48 * Command 'unbundle' is like 'include', but works within a local theory |
|
49 context. Unlike "context includes ... begin", the effect of 'unbundle' |
|
50 on the target context persists, until different declarations are given. |
47 |
51 |
48 |
52 |
49 *** Prover IDE -- Isabelle/Scala/jEdit *** |
53 *** Prover IDE -- Isabelle/Scala/jEdit *** |
50 |
54 |
51 * Cartouche abbreviations work both for " and ` to accomodate typical |
55 * Cartouche abbreviations work both for " and ` to accomodate typical |