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