ETCSprover/conv.sig at master · u5943321/ETCSprover · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
signature conv =
sig

(*
type conv = abbrev.conv
type fconv = abbrev.fconv
*)
include abbrev
val all_conv: conv
val all_fconv: fconv
val arg_conv: conv -> conv
val depth_conv: conv -> conv
val first_conv: conv list -> conv
val no_conv: conv
val orelsec: conv * conv -> conv
val part_fmatch: (thm -> form) -> thm -> fconv
val part_tmatch: (thm -> term) -> thm -> conv
val redepth_conv: conv -> conv
val repeatc: conv -> conv
val rewr_conv: thm -> conv
val rewr_fconv: thm -> fconv
(*val sub_conv: conv -> conv*)
val thenc: conv * conv -> conv
val thenfc: fconv * fconv -> fconv
val top_depth_conv: conv -> conv
val once_depth_conv: conv -> conv
val try_conv: conv -> conv
val basic_fconv: conv -> fconv -> fconv
val basic_taut_fconv: fconv
val changed_fconv: fconv -> fconv
val changed_conv: conv -> conv
val conj_fconv: fconv -> fconv
val depth_fconv: conv -> fconv -> fconv
val dimp_fconv: fconv -> fconv
val disj_fconv: fconv -> fconv
val first_fconv: fconv list -> fconv
val imp_fconv: fconv -> fconv
val no_fconv: fconv
val orelsefc: fconv * fconv -> fconv
val pred_fconv: conv -> fconv
val neg_fconv: fconv -> fconv
val forall_fconv: fconv -> fconv
val exists_fconv: fconv -> fconv
val redepth_fconv: conv -> fconv -> fconv
val refl_fconv: fconv
val repeatfc: fconv -> fconv
val sub_fconv: conv -> fconv -> fconv
val taut_conj_fconv: fconv
val taut_disj_fconv: fconv
val taut_exists_fconv: fconv
val taut_forall_fconv: fconv
val taut_imp_fconv: fconv
val taut_dimp_fconv: fconv
val top_depth_fconv: conv -> fconv -> fconv
val once_depth_fconv: conv -> fconv -> fconv
val basic_once_fconv: conv -> fconv -> fconv
val try_fconv: fconv -> fconv
val simp_trace: bool ref
val conv_rule: fconv -> thm -> thm
val GSYM: thm -> thm
val right_imp_forall_fconv: fconv
val sym_fconv: fconv
val double_neg_fconv: fconv
val neg_neg_elim: thm -> thm

val land_conv: conv -> conv
val rand_conv: conv -> conv

val land_fconv: conv -> fconv -> fconv
val rand_fconv: conv -> fconv -> fconv
end