NEWS
changeset 63273 302daf918966
parent 63272 6d8a67a77bad
child 63282 7c509ddf29a5
equal deleted inserted replaced
63272:6d8a67a77bad 63273:302daf918966
    33 * New symbol \<circle>, e.g. for temporal operator.
    33 * New symbol \<circle>, e.g. for temporal operator.
    34 
    34 
    35 * Old 'header' command is no longer supported (legacy since
    35 * Old 'header' command is no longer supported (legacy since
    36 Isabelle2015).
    36 Isabelle2015).
    37 
    37 
    38 * Command 'bundle_definition' provides a local theory target to define a
    38 * Command 'bundle' provides a local theory target to define a bundle
    39 bundle from the body of specification commands (e.g. 'declare',
    39 from the body of specification commands (such as 'declare',
    40 'declaration', 'notation', 'lemmas', 'lemma').
    40 'declaration', 'notation', 'lemmas', 'lemma'). For example:
       
    41 
       
    42 bundle foo
       
    43 begin
       
    44   declare a [simp]
       
    45   declare b [intro]
       
    46 end
    41 
    47 
    42 
    48 
    43 *** Prover IDE -- Isabelle/Scala/jEdit ***
    49 *** Prover IDE -- Isabelle/Scala/jEdit ***
    44 
    50 
    45 * Cartouche abbreviations work both for " and ` to accomodate typical
    51 * Cartouche abbreviations work both for " and ` to accomodate typical