Declare ML Module "autocontra".

Grammar tactic simple_tactic :=
	[ "Auto_Contra" identarg($id)] ->
	[(TRY (auto_contra $id))].

Syntax tactic pp_auto_contra (TRY (auto_contra $id)) 0
 "Auto_Contra " <$id:"namehyp":*>.

Grammar tactic simple_tactic :=
	[ "Auto_Contra"] ->
	[(TRY (auto_contran))].

Syntax tactic pp_auto_contran (TRY (autocontran)) 0
 "Auto_Contra".