3 Author: Konrad Slind, Cambridge University Computer Laboratory
4 Copyright 1997 University of Cambridge
6 Emulation of HOL inference rules for TFL
11 (* structure USyntax : USyntax_sig *)
12 val dest_thm : thm -> term list * term
15 val REFL :cterm -> thm
16 val ASSUME :cterm -> thm
17 val MP :thm -> thm -> thm
18 val MATCH_MP :thm -> thm -> thm
19 val CONJUNCT1 :thm -> thm
20 val CONJUNCT2 :thm -> thm
21 val CONJUNCTS :thm -> thm list
22 val DISCH :cterm -> thm -> thm
23 val UNDISCH :thm -> thm
24 val INST_TYPE :(typ*typ)list -> thm -> thm
25 val SPEC :cterm -> thm -> thm
26 val ISPEC :cterm -> thm -> thm
27 val ISPECL :cterm list -> thm -> thm
28 val GEN :cterm -> thm -> thm
29 val GENL :cterm list -> thm -> thm
30 val LIST_CONJ :thm list -> thm
33 val DISCH_ALL : thm -> thm
34 val FILTER_DISCH_ALL : (term -> bool) -> thm -> thm
35 val SPEC_ALL : thm -> thm
36 val GEN_ALL : thm -> thm
37 val IMP_TRANS : thm -> thm -> thm
38 val PROVE_HYP : thm -> thm -> thm
40 val CHOOSE : cterm * thm -> thm -> thm
41 val EXISTS : cterm * cterm -> thm -> thm
42 val EXISTL : cterm list -> thm -> thm
43 val IT_EXISTS : (cterm*cterm) list -> thm -> thm
45 val EVEN_ORS : thm list -> thm list
46 val DISJ_CASESL : thm -> thm list -> thm
48 val list_beta_conv : cterm -> cterm list -> thm
49 val SUBS : thm list -> thm -> thm
50 val simpl_conv : simpset -> thm list -> cterm -> thm
52 val rbeta : thm -> thm
53 (* For debugging my isabelle solver in the conditional rewriter *)
54 val term_ref : term list ref
55 val thm_ref : thm list ref
56 val mss_ref : meta_simpset list ref
57 val tracing : bool ref
58 val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
59 -> thm -> thm * term list
60 val RIGHT_ASSOC : thm -> thm
62 val prove : cterm * tactic -> thm