blob: b4e023cde4204a687a68368d2534e4a36c4f6db0 (
plain)
1
2
3
4
5
6
7
8
9
10
|
(* $Id$ *)
Declare ML Module "refine".
Grammar tactic simple_tactic: Ast :=
tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)].
Syntax tactic level 0:
tcc [(Tcc $C)] -> ["Refine " $C].
|