equal
deleted
inserted
replaced
467 ; |
467 ; |
468 @{syntax_def structured_spec}: |
468 @{syntax_def structured_spec}: |
469 @{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes} |
469 @{syntax thmdecl}? @{syntax prop} @{syntax spec_prems} @{syntax for_fixes} |
470 ; |
470 ; |
471 @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))? |
471 @{syntax_def spec_prems}: (@'if' ((@{syntax prop}+) + @'and'))? |
|
472 ; |
|
473 @{syntax_def specification}: @{syntax "fixes"} @'where' @{syntax multi_specs} |
472 \<close>} |
474 \<close>} |
473 \<close> |
475 \<close> |
474 |
476 |
475 |
477 |
476 section \<open>Diagnostic commands\<close> |
478 section \<open>Diagnostic commands\<close> |