blob: ab6ad8fd961c24149b63b70a19548d906dfa5645 (
plain)
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
theory AHundredTheorems
imports Main
begin
(* test this *)
ML {* val start = Timing.start () *}
(* ELISP: -- (setq start (current-time)) -- *)
lemma foo: "P --> P" by auto
lemma foo2: "P --> P" by auto
lemma foo3: "P --> P" by auto
lemma foo4: "P --> P" by auto
lemma foo5: "P --> P" by auto
lemma foo6: "P --> P" by auto
lemma foo7: "P --> P" by auto
lemma foo8: "P --> P" by auto
lemma foo9: "P --> P" by auto
lemma foo10: "P --> P" by auto
lemma foo11: "P --> P" by auto
lemma foo12: "P --> P" by auto
lemma foo13: "P --> P" by auto
lemma foo14: "P --> P" by auto
lemma foo15: "P --> P" by auto
lemma foo16: "P --> P" by auto
lemma foo17: "P --> P" by auto
lemma foo18: "P --> P" by auto
lemma foo19: "P --> P" by auto
lemma foo20: "P --> P" by auto
lemma foo21: "P --> P" by auto
lemma foo22: "P --> P" by auto
lemma foo23: "P --> P" by auto
lemma foo24: "P --> P" by auto
lemma foo25: "P --> P" by auto
lemma foo26: "P --> P" by auto
lemma foo27: "P --> P" by auto
lemma foo28: "P --> P" by auto
lemma foo29: "P --> P" by auto
lemma foo30: "P --> P" by auto
lemma foo31: "P --> P" by auto
lemma foo32: "P --> P" by auto
lemma foo33: "P --> P" by auto
lemma foo34: "P --> P" by auto
lemma foo35: "P --> P" by auto
lemma foo36: "P --> P" by auto
lemma foo37: "P --> P" by auto
lemma foo38: "P --> P" by auto
lemma foo39: "P --> P" by auto
lemma foo40: "P --> P" by auto
lemma foo41: "P --> P" by auto
lemma foo42: "P --> P" by auto
lemma foo43: "P --> P" by auto
lemma foo44: "P --> P" by auto
lemma foo45: "P --> P" by auto
lemma foo46: "P --> P" by auto
lemma foo47: "P --> P" by auto
lemma foo48: "P --> P" by auto
lemma foo49: "P --> P" by auto
lemma foo50: "P --> P" by auto
lemma foo51: "P --> P" by auto
lemma foo52: "P --> P" by auto
lemma foo53: "P --> P" by auto
lemma foo54: "P --> P" by auto
lemma foo55: "P --> P" by auto
lemma foo56: "P --> P" by auto
lemma foo57: "P --> P" by auto
lemma foo58: "P --> P" by auto
lemma foo59: "P --> P" by auto
lemma foo60: "P --> P" by auto
lemma foo61: "P --> P" by auto
lemma foo62: "P --> P" by auto
lemma foo63: "P --> P" by auto
lemma foo64: "P --> P" by auto
lemma foo65: "P --> P" by auto
lemma foo66: "P --> P" by auto
lemma foo67: "P --> P" by auto
lemma foo68: "P --> P" by auto
lemma foo69: "P --> P" by auto
lemma foo70: "P --> P" by auto
lemma foo71: "P --> P" by auto
lemma foo72: "P --> P" by auto
lemma foo73: "P --> P" by auto
lemma foo74: "P --> P" by auto
lemma foo75: "P --> P" by auto
lemma foo76: "P --> P" by auto
lemma foo77: "P --> P" by auto
lemma foo78: "P --> P" by auto
lemma foo79: "P --> P" by auto
lemma foo80: "P --> P" by auto
lemma foo81: "P --> P" by auto
lemma foo82: "P --> P" by auto
lemma foo83: "P --> P" by auto
lemma foo84: "P --> P" by auto
lemma foo85: "P --> P" by auto
lemma foo86: "P --> P" by auto
lemma foo87: "P --> P" by auto
lemma foo88: "P --> P" by auto
lemma foo89: "P --> P" by auto
lemma foo90: "P --> P" by auto
lemma foo91: "P --> P" by auto
lemma foo92: "P --> P" by auto
lemma foo93: "P --> P" by auto
lemma foo94: "P --> P" by auto
lemma foo95: "P --> P" by auto
lemma foo96: "P --> P" by auto
lemma foo97: "P --> P" by auto
lemma foo98: "P --> P" by auto
lemma foo99: "P --> P" by auto
lemma foo100: "P --> P" by auto
(* NB: this doesn't work because of comment aggregation *)
(* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *)
ML {* warning (Timing.message (Timing.result start)) *}
end
|
