]> matita.cs.unibo.it Git - helm.git/blob - variousTactics.mli
2be47c1ec25205fff13e7344bf9337afb458209f
[helm.git] / variousTactics.mli
1
2 (* Copyright (C) 2002, HELM Team.
3  * 
4  * This file is part of HELM, an Hypertextual, Electronic
5  * Library of Mathematics, developed at the Computer Science
6  * Department, University of Bologna, Italy.
7  * 
8  * HELM is free software; you can redistribute it and/or
9  * modify it under the terms of the GNU General Public License
10  * as published by the Free Software Foundation; either version 2
11  * of the License, or (at your option) any later version.
12  * 
13  * HELM is distributed in the hope that it will be useful,
14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16  * GNU General Public License for more details.
17  *
18  * You should have received a copy of the GNU General Public License
19  * along with HELM; if not, write to the Free Software
20  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
21  * MA  02111-1307, USA.
22  * 
23  * For details, see the HELM World-Wide-Web page,
24  * http://cs.unibo.it/helm/.
25  *)
26
27 exception AllSelectedTermsMustBeConvertible;;
28 exception NotApplicableTheorem;;
29
30 val assumption_tac: ProofEngineTypes.tactic
31 val generalize_tac:
32  ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term list ->
33   ProofEngineTypes.tactic
34
35 val auto_tac : 
36  MQIConn.handle -> 
37  status:ProofEngineTypes.status 
38   -> ProofEngineTypes.proof * ProofEngineTypes.goal list