equal
deleted
inserted
replaced
282 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
282 @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
283 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
283 @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\ |
284 \end{matharray} |
284 \end{matharray} |
285 |
285 |
286 \begin{rail} |
286 \begin{rail} |
287 ( 'rule\_tac' | 'erule\_tac' | 'drule\_tac' | 'frule\_tac' | 'cut\_tac' | 'thin\_tac' ) goalspec? |
287 ( 'rule_tac' | 'erule_tac' | 'drule_tac' | 'frule_tac' | 'cut_tac' | 'thin_tac' ) goalspec? |
288 ( insts thmref | thmrefs ) |
288 ( insts thmref | thmrefs ) |
289 ; |
289 ; |
290 'subgoal\_tac' goalspec? (prop +) |
290 'subgoal_tac' goalspec? (prop +) |
291 ; |
291 ; |
292 'rename\_tac' goalspec? (name +) |
292 'rename_tac' goalspec? (name +) |
293 ; |
293 ; |
294 'rotate\_tac' goalspec? int? |
294 'rotate_tac' goalspec? int? |
295 ; |
295 ; |
296 ('tactic' | 'raw_tactic') text |
296 ('tactic' | 'raw_tactic') text |
297 ; |
297 ; |
298 |
298 |
299 insts: ((name '=' term) + 'and') 'in' |
299 insts: ((name '=' term) + 'and') 'in' |
362 @{method_def simp_all} & : & @{text method} \\ |
362 @{method_def simp_all} & : & @{text method} \\ |
363 \end{matharray} |
363 \end{matharray} |
364 |
364 |
365 \indexouternonterm{simpmod} |
365 \indexouternonterm{simpmod} |
366 \begin{rail} |
366 \begin{rail} |
367 ('simp' | 'simp\_all') opt? (simpmod *) |
367 ('simp' | 'simp_all') opt? (simpmod *) |
368 ; |
368 ; |
369 |
369 |
370 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')' |
370 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use' | 'asm_lr' ) ')' |
371 ; |
371 ; |
372 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
372 simpmod: ('add' | 'del' | 'only' | 'cong' (() | 'add' | 'del') | |
373 'split' (() | 'add' | 'del')) ':' thmrefs |
373 'split' (() | 'add' | 'del')) ':' thmrefs |
374 ; |
374 ; |
375 \end{rail} |
375 \end{rail} |
469 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
469 @{command_def "simproc_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\ |
470 simproc & : & @{text attribute} \\ |
470 simproc & : & @{text attribute} \\ |
471 \end{matharray} |
471 \end{matharray} |
472 |
472 |
473 \begin{rail} |
473 \begin{rail} |
474 'simproc\_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))? |
474 'simproc_setup' name '(' (term + '|') ')' '=' text \\ ('identifier' (nameref+))? |
475 ; |
475 ; |
476 |
476 |
477 'simproc' (('add' ':')? | 'del' ':') (name+) |
477 'simproc' (('add' ':')? | 'del' ':') (name+) |
478 ; |
478 ; |
479 \end{rail} |
479 \end{rail} |
517 |
517 |
518 \begin{rail} |
518 \begin{rail} |
519 'simplified' opt? thmrefs? |
519 'simplified' opt? thmrefs? |
520 ; |
520 ; |
521 |
521 |
522 opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use') ')' |
522 opt: '(' ('no_asm' | 'no_asm_simp' | 'no_asm_use') ')' |
523 ; |
523 ; |
524 \end{rail} |
524 \end{rail} |
525 |
525 |
526 \begin{description} |
526 \begin{description} |
527 |
527 |
783 \begin{rail} |
783 \begin{rail} |
784 'judgment' constdecl |
784 'judgment' constdecl |
785 ; |
785 ; |
786 'atomize' ('(' 'full' ')')? |
786 'atomize' ('(' 'full' ')')? |
787 ; |
787 ; |
788 'rule\_format' ('(' 'noasm' ')')? |
788 'rule_format' ('(' 'noasm' ')')? |
789 ; |
789 ; |
790 \end{rail} |
790 \end{rail} |
791 |
791 |
792 \begin{description} |
792 \begin{description} |
793 |
793 |