blob: c6283109c15752e24bcc088bd31eb076203031b1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* $Id$ *)
Declare ML Module "tauto".
Grammar tactic simple_tactic: ast :=
tauto [ "Tauto" ] -> [(Tauto)]
| intuition [ "Intuition" ] -> [(Intuition)].
Syntax tactic level 0:
tauto [(Tauto)] -> ["Tauto"]
| intuition [(Intuition)] -> ["Intuition"].
|
