blob: 40a4a048b66e5542eb2759db7467010a927eca28 (
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"].
|
