/[mojave]/metaprl/theories/czf/czf_itt_abel_group.prla
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_abel_group.prla

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3554 by xiny, Sun Mar 24 07:43:47 2002 UTC revision 3555 by xiny, Tue Apr 2 07:49:49 2002 UTC
# Line 5  Line 5 
5  NSummary        Summary Summary NIL  NSummary        Summary Summary NIL
6  NSummary!location       location        location Summary  NSummary!location       location        location Summary
7  P       p       Number 0  P       p       Number 0
8  P       p4      Number 19  P       p1      Number 19
9  O       o8      location p p4  O       o1      location p p1
10  NSummary!parent parent  parent Summary  NSummary!parent parent  parent Summary
11  O       o2      parent  O       o2      parent
12  P       p2      String Czf_itt_group  P       p2      String Czf_itt_set
13  O       o3      parent p2  O       o3      parent p2
14  T       t       o3  T       t       o3
15  B       b       t  B       b       t
# Line 19  Line 19 
19  B       b4      t4  B       b4      t4
20  T       t5      o b b4  T       t5      o b b4
21  B       b5      t5  B       b5      t5
22  P       p5      String Czf_itt_and  P       p5      String Czf_itt_comment
23  O       o5      parent p5  O       o5      parent p5
24  T       t6      o5  T       t6      o5
25  B       b6      t6  B       b6      t6
26  T       t7      o b6 b4  T       t7      o b6 b4
27  B       b7      t7  B       b7      t7
28  P       p7      String Czf_itt_dall  P       p7      String Itt_theory
29  O       o7      parent p7  O       o7      parent p7
30  T       t8      o7  T       t8      o7
31  B       b8      t8  B       b8      t8
32  T       t9      o b8 b4  T       t9      o b8 b4
33  B       b9      t9  B       b9      t9
34  P       p9      String Czf_itt_set_ind  P       p9      String Itt_fset
35  O       o9      parent p9  O       o9      parent p9
36  T       t10     o9  T       t10     o9
37  B       b10     t10  B       b10     t10
38  T       t11     o b10 b4  T       t11     o b10 b4
39  B       b11     t11  B       b11     t11
40  P       p11     String Czf_itt_all  P       p11     String Itt_prop_decide
41  O       o11     parent p11  O       o11     parent p11
42  T       t12     o11  T       t12     o11
43  B       b12     t12  B       b12     t12
44  T       t13     o b12 b4  T       t13     o b12 b4
45  B       b13     t13  B       b13     t13
46  P       p13     String Czf_itt_sep  P       p13     String Itt_derive
47  O       o13     parent p13  O       o13     parent p13
48  T       t14     o13  T       t14     o13
49  B       b14     t14  B       b14     t14
50  T       t15     o b14 b4  T       t15     o b14 b4
51  B       b15     t15  B       b15     t15
52  P       p15     String Czf_itt_member  P       p15     String Itt_list2
53  O       o15     parent p15  O       o15     parent p15
54  T       t16     o15  T       t16     o15
55  B       b16     t16  B       b16     t16
56  T       t17     o b16 b4  T       t17     o b16 b4
57  B       b17     t17  B       b17     t17
58  P       p17     String Czf_itt_eq  P       p17     String Itt_list
59  O       o17     parent p17  O       o17     parent p17
60  T       t18     o17  T       t18     o17
61  B       b18     t18  B       b18     t18
62  T       t19     o b18 b4  T       t19     o b18 b4
63  B       b19     t19  B       b19     t19
64  P       p19     String Czf_itt_set  P       p19     String Itt_quotient
65  O       o19     parent p19  O       o19     parent p19
66  T       t20     o19  T       t20     o19
67  B       b20     t20  B       b20     t20
68  T       t21     o b20 b4  T       t21     o b20 b4
69  B       b21     t21  B       b21     t21
70  P       p21     String Czf_itt_comment  P       p21     String Itt_esquash
71  O       o21     parent p21  O       o21     parent p21
72  T       t22     o21  T       t22     o21
73  B       b22     t22  B       b22     t22
74  T       t23     o b22 b4  T       t23     o b22 b4
75  B       b23     t23  B       b23     t23
76  P       p23     String Itt_theory  P       p23     String Itt_srec
77  O       o23     parent p23  O       o23     parent p23
78  T       t24     o23  T       t24     o23
79  B       b24     t24  B       b24     t24
80  T       t25     o b24 b4  T       t25     o b24 b4
81  B       b25     t25  B       b25     t25
82  P       p25     String Itt_fset  P       p25     String Itt_prec
83  O       o25     parent p25  O       o25     parent p25
84  T       t26     o25  T       t26     o25
85  B       b26     t26  B       b26     t26
86  T       t27     o b26 b4  T       t27     o b26 b4
87  B       b27     t27  B       b27     t27
88  P       p27     String Itt_prop_decide  P       p27     String Itt_w
89  O       o27     parent p27  O       o27     parent p27
90  T       t28     o27  T       t28     o27
91  B       b28     t28  B       b28     t28
92  T       t29     o b28 b4  T       t29     o b28 b4
93  B       b29     t29  B       b29     t29
94  P       p29     String Itt_derive  P       p29     String Itt_bunion
95  O       o29     parent p29  O       o29     parent p29
96  T       t30     o29  T       t30     o29
97  B       b30     t30  B       b30     t30
98  T       t31     o b30 b4  T       t31     o b30 b4
99  B       b31     t31  B       b31     t31
100  P       p31     String Itt_list2  P       p31     String Itt_bisect
101  O       o31     parent p31  O       o31     parent p31
102  T       t32     o31  T       t32     o31
103  B       b32     t32  B       b32     t32
104  T       t33     o b32 b4  T       t33     o b32 b4
105  B       b33     t33  B       b33     t33
106  P       p33     String Itt_list  P       p33     String Itt_tunion
107  O       o33     parent p33  O       o33     parent p33
108  T       t34     o33  T       t34     o33
109  B       b34     t34  B       b34     t34
110  T       t35     o b34 b4  T       t35     o b34 b4
111  B       b35     t35  B       b35     t35
112  P       p35     String Itt_quotient  P       p35     String Itt_isect
113  O       o35     parent p35  O       o35     parent p35
114  T       t36     o35  T       t36     o35
115  B       b36     t36  B       b36     t36
116  T       t37     o b36 b4  T       t37     o b36 b4
117  B       b37     t37  B       b37     t37
118  P       p37     String Itt_esquash  P       p37     String Itt_struct2
119  O       o37     parent p37  O       o37     parent p37
120  T       t38     o37  T       t38     o37
121  B       b38     t38  B       b38     t38
122  T       t39     o b38 b4  T       t39     o b38 b4
123  B       b39     t39  B       b39     t39
124  P       p39     String Itt_srec  P       p39     String Itt_well_founded
125  O       o39     parent p39  O       o39     parent p39
126  T       t40     o39  T       t40     o39
127  B       b40     t40  B       b40     t40
128  T       t41     o b40 b4  T       t41     o b40 b4
129  B       b41     t41  B       b41     t41
130  P       p41     String Itt_prec  P       p41     String Itt_int_arith
131  O       o41     parent p41  O       o41     parent p41
132  T       t42     o41  T       t42     o41
133  B       b42     t42  B       b42     t42
134  T       t43     o b42 b4  T       t43     o b42 b4
135  B       b43     t43  B       b43     t43
136  P       p43     String Itt_w  P       p43     String Itt_int_ext
137  O       o43     parent p43  O       o43     parent p43
138  T       t44     o43  T       t44     o43
139  B       b44     t44  B       b44     t44
140  T       t45     o b44 b4  T       t45     o b44 b4
141  B       b45     t45  B       b45     t45
142  P       p45     String Itt_bunion  P       p45     String Itt_int_base
143  O       o45     parent p45  O       o45     parent p45
144  T       t46     o45  T       t46     o45
145  B       b46     t46  B       b46     t46
146  T       t47     o b46 b4  T       t47     o b46 b4
147  B       b47     t47  B       b47     t47
148  P       p47     String Itt_bisect  P       p47     String Itt_atom_bool
149  O       o47     parent p47  O       o47     parent p47
150  T       t48     o47  T       t48     o47
151  B       b48     t48  B       b48     t48
152  T       t49     o b48 b4  T       t49     o b48 b4
153  B       b49     t49  B       b49     t49
154  P       p49     String Itt_tunion  P       p49     String Itt_atom
155  O       o49     parent p49  O       o49     parent p49
156  T       t50     o49  T       t50     o49
157  B       b50     t50  B       b50     t50
158  T       t51     o b50 b4  T       t51     o b50 b4
159  B       b51     t51  B       b51     t51
160  P       p51     String Itt_isect  P       p51     String Itt_bool
161  O       o51     parent p51  O       o51     parent p51
162  T       t52     o51  T       t52     o51
163  B       b52     t52  B       b52     t52
164  T       t53     o b52 b4  T       t53     o b52 b4
165  B       b53     t53  B       b53     t53
166  P       p53     String Itt_struct2  P       p53     String Itt_decidable
167  O       o53     parent p53  O       o53     parent p53
168  T       t54     o53  T       t54     o53
169  B       b54     t54  B       b54     t54
170  T       t55     o b54 b4  T       t55     o b54 b4
171  B       b55     t55  B       b55     t55
172  P       p55     String Itt_well_founded  P       p55     String Itt_logic
173  O       o55     parent p55  O       o55     parent p55
174  T       t56     o55  T       t56     o55
175  B       b56     t56  B       b56     t56
176  T       t57     o b56 b4  T       t57     o b56 b4
177  B       b57     t57  B       b57     t57
178  P       p57     String Itt_int_arith  P       p57     String Itt_prod
179  O       o57     parent p57  O       o57     parent p57
180  T       t58     o57  T       t58     o57
181  B       b58     t58  B       b58     t58
182  T       t59     o b58 b4  T       t59     o b58 b4
183  B       b59     t59  B       b59     t59
184  P       p59     String Itt_int_ext  P       p59     String Itt_dprod
185  O       o59     parent p59  O       o59     parent p59
186  T       t60     o59  T       t60     o59
187  B       b60     t60  B       b60     t60
188  T       t61     o b60 b4  T       t61     o b60 b4
189  B       b61     t61  B       b61     t61
190  P       p61     String Itt_int_base  P       p61     String Itt_fun
191  O       o61     parent p61  O       o61     parent p61
192  T       t62     o61  T       t62     o61
193  B       b62     t62  B       b62     t62
194  T       t63     o b62 b4  T       t63     o b62 b4
195  B       b63     t63  B       b63     t63
196  P       p63     String Itt_atom_bool  P       p63     String Itt_dfun
197  O       o63     parent p63  O       o63     parent p63
198  T       t64     o63  T       t64     o63
199  B       b64     t64  B       b64     t64
200  T       t65     o b64 b4  T       t65     o b64 b4
201  B       b65     t65  B       b65     t65
202  P       p65     String Itt_atom  P       p65     String Itt_rfun
203  O       o65     parent p65  O       o65     parent p65
204  T       t66     o65  T       t66     o65
205  B       b66     t66  B       b66     t66
206  T       t67     o b66 b4  T       t67     o b66 b4
207  B       b67     t67  B       b67     t67
208  P       p3      String Itt_record_label0  P       p67     String Itt_set
 O       o6      parent p3  
 T       t238    o6  
 B       b238    t238  
 T       t239    o b238 b4  
 B       b239    t239  
 P       p248    String Itt_nat  
 O       o248    parent p248  
 T       t253    o248  
 B       b253    t253  
 T       t254    o b253 b4  
 B       b254    t254  
 P       p67     String Itt_bool  
209  O       o67     parent p67  O       o67     parent p67
210  T       t68     o67  T       t68     o67
211  B       b68     t68  B       b68     t68
212  T       t69     o b68 b4  T       t69     o b68 b4
213  B       b69     t69  B       b69     t69
214  P       p69     String Itt_decidable  P       p69     String Itt_unit
215  O       o69     parent p69  O       o69     parent p69
216  T       t70     o69  T       t70     o69
217  B       b70     t70  B       b70     t70
218  T       t71     o b70 b4  T       t71     o b70 b4
219  B       b71     t71  B       b71     t71
220  P       p71     String Itt_logic  P       p71     String Itt_squiggle
221  O       o71     parent p71  O       o71     parent p71
222  T       t72     o71  T       t72     o71
223  B       b72     t72  B       b72     t72
224  T       t73     o b72 b4  T       t73     o b72 b4
225  B       b73     t73  B       b73     t73
226  P       p73     String Itt_prod  P       p73     String Itt_squash
227  O       o73     parent p73  O       o73     parent p73
228  T       t74     o73  T       t74     o73
229  B       b74     t74  B       b74     t74
230  T       t75     o b74 b4  T       t75     o b74 b4
231  B       b75     t75  B       b75     t75
232  P       p75     String Itt_dprod  P       p75     String Itt_union
233  O       o75     parent p75  O       o75     parent p75
234  T       t76     o75  T       t76     o75
235  B       b76     t76  B       b76     t76
236  T       t77     o b76 b4  T       t77     o b76 b4
237  B       b77     t77  B       b77     t77
238  P       p77     String Itt_fun  P       p77     String Itt_void
239  O       o77     parent p77  O       o77     parent p77
240  T       t78     o77  T       t78     o77
241  B       b78     t78  B       b78     t78
242  T       t79     o b78 b4  T       t79     o b78 b4
243  B       b79     t79  B       b79     t79
244  P       p79     String Itt_dfun  P       p79     String Itt_subtype
245  O       o79     parent p79  O       o79     parent p79
246  T       t80     o79  T       t80     o79
247  B       b80     t80  B       b80     t80
248  T       t81     o b80 b4  T       t81     o b80 b4
249  B       b81     t81  B       b81     t81
250  P       p81     String Itt_rfun  P       p81     String Itt_struct
251  O       o81     parent p81  O       o81     parent p81
252  T       t82     o81  T       t82     o81
253  B       b82     t82  B       b82     t82
254  T       t83     o b82 b4  T       t83     o b82 b4
255  B       b83     t83  B       b83     t83
256  P       p83     String Itt_set  P       p83     String Itt_equal
257  O       o83     parent p83  O       o83     parent p83
258  T       t84     o83  T       t84     o83
259  B       b84     t84  B       b84     t84
260  T       t85     o b84 b4  T       t85     o b84 b4
261  B       b85     t85  B       b85     t85
262  P       p85     String Itt_unit  P       p85     String Itt_comment
263  O       o85     parent p85  O       o85     parent p85
264  T       t86     o85  T       t86     o85
265  B       b86     t86  B       b86     t86
266  T       t87     o b86 b4  T       t87     o b86 b4
267  B       b87     t87  B       b87     t87
268  P       p87     String Itt_squiggle  P       p87     String Base_theory
269  O       o87     parent p87  O       o87     parent p87
270  T       t88     o87  T       t88     o87
271  B       b88     t88  B       b88     t88
272  T       t89     o b88 b4  T       t89     o b88 b4
273  B       b89     t89  B       b89     t89
274  P       p89     String Itt_squash  P       p89     String Base_meta
275  O       o89     parent p89  O       o89     parent p89
276  T       t90     o89  T       t90     o89
277  B       b90     t90  B       b90     t90
278  T       t91     o b90 b4  T       t91     o b90 b4
279  B       b91     t91  B       b91     t91
280  P       p91     String Itt_union  P       p91     String Base_cache
281  O       o91     parent p91  O       o91     parent p91
282  T       t92     o91  T       t92     o91
283  B       b92     t92  B       b92     t92
284  T       t93     o b92 b4  T       t93     o b92 b4
285  B       b93     t93  B       b93     t93
286  P       p93     String Itt_void  P       p93     String Tactic_cache
287  O       o93     parent p93  O       o93     parent p93
288  T       t94     o93  T       t94     o93
289  B       b94     t94  B       b94     t94
290  T       t95     o b94 b4  T       t95     o b94 b4
291  B       b95     t95  B       b95     t95
292  P       p95     String Itt_subtype  P       p95     String Typeinf
293  O       o95     parent p95  O       o95     parent p95
294  T       t96     o95  T       t96     o95
295  B       b96     t96  B       b96     t96
296  T       t97     o b96 b4  T       t97     o b96 b4
297  B       b97     t97  B       b97     t97
298  P       p97     String Itt_struct  P       p97     String Ocaml_df
299  O       o97     parent p97  O       o97     parent p97
300  T       t98     o97  T       t98     o97
301  B       b98     t98  B       b98     t98
302  T       t99     o b98 b4  T       t99     o b98 b4
303  B       b99     t99  B       b99     t99
304  P       p99     String Itt_equal  P       p99     String Ocaml_str_df
305  O       o99     parent p99  O       o99     parent p99
306  T       t100    o99  T       t100    o99
307  B       b100    t100  B       b100    t100
308  T       t101    o b100 b4  T       t101    o b100 b4
309  B       b101    t101  B       b101    t101
310  P       p101    String Itt_comment  P       p101    String Ocaml_sig_df
311  O       o101    parent p101  O       o101    parent p101
312  T       t102    o101  T       t102    o101
313  B       b102    t102  B       b102    t102
314  T       t103    o b102 b4  T       t103    o b102 b4
315  B       b103    t103  B       b103    t103
316  P       p103    String Base_theory  P       p103    String Ocaml_me_df
317  O       o103    parent p103  O       o103    parent p103
318  T       t104    o103  T       t104    o103
319  B       b104    t104  B       b104    t104
320  T       t105    o b104 b4  T       t105    o b104 b4
321  B       b105    t105  B       b105    t105
322  P       p105    String Base_meta  P       p105    String Ocaml_mt_df
323  O       o105    parent p105  O       o105    parent p105
324  T       t106    o105  T       t106    o105
325  B       b106    t106  B       b106    t106
326  T       t107    o b106 b4  T       t107    o b106 b4
327  B       b107    t107  B       b107    t107
328  P       p107    String Base_cache  P       p107    String Ocaml_type_df
329  O       o107    parent p107  O       o107    parent p107
330  T       t108    o107  T       t108    o107
331  B       b108    t108  B       b108    t108
332  T       t109    o b108 b4  T       t109    o b108 b4
333  B       b109    t109  B       b109    t109
334  P       p109    String Tactic_cache  P       p109    String Ocaml_patt_df
335  O       o109    parent p109  O       o109    parent p109
336  T       t110    o109  T       t110    o109
337  B       b110    t110  B       b110    t110
338  T       t111    o b110 b4  T       t111    o b110 b4
339  B       b111    t111  B       b111    t111
340  P       p111    String Typeinf  P       p111    String Ocaml_expr_df
341  O       o111    parent p111  O       o111    parent p111
342  T       t112    o111  T       t112    o111
343  B       b112    t112  B       b112    t112
344  T       t113    o b112 b4  T       t113    o b112 b4
345  B       b113    t113  B       b113    t113
346  P       p113    String Ocaml_df  P       p113    String Ocaml_base_df
347  O       o113    parent p113  O       o113    parent p113
348  T       t114    o113  T       t114    o113
349  B       b114    t114  B       b114    t114
350  T       t115    o b114 b4  T       t115    o b114 b4
351  B       b115    t115  B       b115    t115
352  P       p115    String Ocaml_str_df  P       p115    String Ocaml
353  O       o115    parent p115  O       o115    parent p115
354  T       t116    o115  T       t116    o115
355  B       b116    t116  B       b116    t116
356  T       t117    o b116 b4  T       t117    o b116 b4
357  B       b117    t117  B       b117    t117
358  P       p117    String Ocaml_sig_df  P       p117    String Base_rewrite
359  O       o117    parent p117  O       o117    parent p117
360  T       t118    o117  T       t118    o117
361  B       b118    t118  B       b118    t118
362  T       t119    o b118 b4  T       t119    o b118 b4
363  B       b119    t119  B       b119    t119
364  P       p119    String Ocaml_me_df  P       p119    String Base_dtactic
365  O       o119    parent p119  O       o119    parent p119
366  T       t120    o119  T       t120    o119
367  B       b120    t120  B       b120    t120
368  T       t121    o b120 b4  T       t121    o b120 b4
369  B       b121    t121  B       b121    t121
370  P       p121    String Ocaml_mt_df  P       p121    String Base_auto_tactic
371  O       o121    parent p121  O       o121    parent p121
372  T       t122    o121  T       t122    o121
373  B       b122    t122  B       b122    t122
374  T       t123    o b122 b4  T       t123    o b122 b4
375  B       b123    t123  B       b123    t123
376  P       p123    String Ocaml_type_df  P       p123    String Base_trivial
377  O       o123    parent p123  O       o123    parent p123
378  T       t124    o123  T       t124    o123
379  B       b124    t124  B       b124    t124
380  T       t125    o b124 b4  T       t125    o b124 b4
381  B       b125    t125  B       b125    t125
382  P       p125    String Ocaml_patt_df  P       p125    String Top_conversionals
383  O       o125    parent p125  O       o125    parent p125
384  T       t126    o125  T       t126    o125
385  B       b126    t126  B       b126    t126
386  T       t127    o b126 b4  T       t127    o b126 b4
387  B       b127    t127  B       b127    t127
388  P       p127    String Ocaml_expr_df  P       p127    String Top_tacticals
389  O       o127    parent p127  O       o127    parent p127
390  T       t128    o127  T       t128    o127
391  B       b128    t128  B       b128    t128
392  T       t129    o b128 b4  T       t129    o b128 b4
393  B       b129    t129  B       b129    t129
394  P       p129    String Ocaml_base_df  P       p129    String Var
395  O       o129    parent p129  O       o129    parent p129
396  T       t130    o129  T       t130    o129
397  B       b130    t130  B       b130    t130
398  T       t131    o b130 b4  T       t131    o b130 b4
399  B       b131    t131  B       b131    t131
400  P       p131    String Ocaml  P       p131    String Mptop
401  O       o131    parent p131  O       o131    parent p131
402  T       t132    o131  T       t132    o131
403  B       b132    t132  B       b132    t132
404  T       t133    o b132 b4  T       t133    o b132 b4
405  B       b133    t133  B       b133    t133
406  P       p133    String Base_rewrite  P       p133    String Summary
407  O       o133    parent p133  O       o133    parent p133
408  T       t134    o133  T       t134    o133
409  B       b134    t134  B       b134    t134
410  T       t135    o b134 b4  T       t135    o b134 b4
411  B       b135    t135  B       b135    t135
412  P       p135    String Base_dtactic  P       p135    String Comment
413  O       o135    parent p135  O       o135    parent p135
414  T       t136    o135  T       t136    o135
415  B       b136    t136  B       b136    t136
416  T       t137    o b136 b4  T       t137    o b136 b4
417  B       b137    t137  B       b137    t137
418  P       p137    String Base_auto_tactic  P       p137    String Base_dform
419  O       o137    parent p137  O       o137    parent p137
420  T       t138    o137  T       t138    o137
421  B       b138    t138  B       b138    t138
422  T       t139    o b138 b4  T       t139    o b138 b4
423  B       b139    t139  B       b139    t139
424  P       p139    String Base_trivial  P       p139    String Nuprl_font
425  O       o139    parent p139  O       o139    parent p139
426  T       t140    o139  T       t140    o139
427  B       b140    t140  B       b140    t140
428  T       t141    o b140 b4  T       t141    o b140 b4
429  B       b141    t141  B       b141    t141
430  P       p141    String Top_conversionals  P       p141    String Perv
431  O       o141    parent p141  O       o141    parent p141
432  T       t142    o141  T       t142    o141
433  B       b142    t142  B       b142    t142
434  T       t143    o b142 b4  T       t143    o b142 b4
435  B       b143    t143  B       b143    t143
436  P       p143    String Top_tacticals  T       t144    o b143 b4
 O       o143    parent p143  
 T       t144    o143  
437  B       b144    t144  B       b144    t144
438  T       t145    o b144 b4  T       t145    o b141 b144
439  B       b145    t145  B       b145    t145
440  P       p145    String Var  T       t146    o b139 b145
 O       o145    parent p145  
 T       t146    o145  
441  B       b146    t146  B       b146    t146
442  T       t147    o b146 b4  T       t147    o b137 b146
443  B       b147    t147  B       b147    t147
444  P       p147    String Mptop  T       t148    o b135 b147
 O       o147    parent p147  
 T       t148    o147  
445  B       b148    t148  B       b148    t148
446  T       t149    o b148 b4  T       t149    o b133 b148
447  B       b149    t149  B       b149    t149
448  P       p149    String Summary  T       t150    o b131 b149
 O       o149    parent p149  
 T       t150    o149  
449  B       b150    t150  B       b150    t150
450  T       t151    o b150 b4  T       t151    o b129 b150
451  B       b151    t151  B       b151    t151
452  P       p151    String Comment  T       t152    o b127 b151
 O       o151    parent p151  
 T       t152    o151  
453  B       b152    t152  B       b152    t152
454  T       t153    o b152 b4  T       t153    o b125 b152
455  B       b153    t153  B       b153    t153
456  P       p153    String Base_dform  T       t154    o b123 b153
 O       o153    parent p153  
 T       t154    o153  
457  B       b154    t154  B       b154    t154
458  T       t155    o b154 b4  T       t155    o b121 b154
459  B       b155    t155  B       b155    t155
460  P       p155    String Nuprl_font  T       t156    o b119 b155
 O       o155    parent p155  
 T       t156    o155  
461  B       b156    t156  B       b156    t156
462  T       t157    o b156 b4  T       t157    o b117 b156
463  B       b157    t157  B       b157    t157
464  P       p157    String Perv  T       t158    o b115 b157
 O       o157    parent p157  
 T       t158    o157  
465  B       b158    t158  B       b158    t158
466  T       t159    o b158 b4  T       t159    o b113 b158
467  B       b159    t159  B       b159    t159
468  T       t160    o b159 b4  T       t160    o b111 b159
469  B       b160    t160  B       b160    t160
470  T       t161    o b157 b160  T       t161    o b109 b160
471  B       b161    t161  B       b161    t161
472  T       t162    o b155 b161  T       t162    o b107 b161
473  B       b162    t162  B       b162    t162
474  T       t163    o b153 b162  T       t163    o b105 b162
475  B       b163    t163  B       b163    t163
476  T       t164    o b151 b163  T       t164    o b103 b163
477  B       b164    t164  B       b164    t164
478  T       t165    o b149 b164  T       t165    o b101 b164
479  B       b165    t165  B       b165    t165
480  T       t166    o b147 b165  T       t166    o b99 b165
481  B       b166    t166  B       b166    t166
482  T       t167    o b145 b166  T       t167    o b97 b166
483  B       b167    t167  B       b167    t167
484  T       t168    o b143 b167  T       t168    o b95 b167
485  B       b168    t168  B       b168    t168
486  T       t169    o b141 b168  T       t169    o b93 b168
487  B       b169    t169  B       b169    t169
488  T       t170    o b139 b169  T       t170    o b91 b169
489  B       b170    t170  B       b170    t170
490  T       t171    o b137 b170  T       t171    o b89 b170
491  B       b171    t171  B       b171    t171
492  T       t172    o b135 b171  T       t172    o b87 b171
493  B       b172    t172  B       b172    t172
494  T       t173    o b133 b172  T       t173    o b85 b172
495  B       b173    t173  B       b173    t173
496  T       t174    o b131 b173  T       t174    o b83 b173
497  B       b174    t174  B       b174    t174
498  T       t175    o b129 b174  T       t175    o b81 b174
499  B       b175    t175  B       b175    t175
500  T       t176    o b127 b175  T       t176    o b79 b175
501  B       b176    t176  B       b176    t176
502  T       t177    o b125 b176  T       t177    o b77 b176
503  B       b177    t177  B       b177    t177
504  T       t178    o b123 b177  T       t178    o b75 b177
505  B       b178    t178  B       b178    t178
506  T       t179    o b121 b178  T       t179    o b73 b178
507  B       b179    t179  B       b179    t179
508  T       t180    o b119 b179  T       t180    o b71 b179
509  B       b180    t180  B       b180    t180
510  T       t181    o b117 b180  T       t181    o b69 b180
511  B       b181    t181  B       b181    t181
512  T       t182    o b115 b181  T       t182    o b67 b181
513  B       b182    t182  B       b182    t182
514  T       t183    o b113 b182  T       t183    o b65 b182
515  B       b183    t183  B       b183    t183
516  T       t184    o b111 b183  T       t184    o b63 b183
517  B       b184    t184  B       b184    t184
518  T       t185    o b109 b184  T       t185    o b61 b184
519  B       b185    t185  B       b185    t185
520  T       t186    o b107 b185  T       t186    o b59 b185
521  B       b186    t186  B       b186    t186
522  T       t187    o b105 b186  T       t187    o b57 b186
523  B       b187    t187  B       b187    t187
524  T       t188    o b103 b187  T       t188    o b55 b187
525  B       b188    t188  B       b188    t188
526  T       t189    o b101 b188  T       t189    o b53 b188
527  B       b189    t189  B       b189    t189
528  T       t190    o b99 b189  T       t190    o b51 b189
529  B       b190    t190  B       b190    t190
530  T       t191    o b97 b190  T       t191    o b49 b190
531  B       b191    t191  B       b191    t191
532  T       t192    o b95 b191  T       t192    o b47 b191
533  B       b192    t192  B       b192    t192
534  T       t193    o b93 b192  T       t193    o b45 b192
535  B       b193    t193  B       b193    t193
536  T       t194    o b91 b193  T       t194    o b43 b193
537  B       b194    t194  B       b194    t194
538  T       t195    o b89 b194  T       t195    o b41 b194
539  B       b195    t195  B       b195    t195
540  T       t196    o b87 b195  T       t196    o b39 b195
541  B       b196    t196  B       b196    t196
542  T       t197    o b85 b196  T       t197    o b37 b196
543  B       b197    t197  B       b197    t197
544  T       t198    o b83 b197  T       t198    o b35 b197
545  B       b198    t198  B       b198    t198
546  T       t199    o b81 b198  T       t199    o b33 b198
547  B       b199    t199  B       b199    t199
548  T       t200    o b79 b199  T       t200    o b31 b199
549  B       b200    t200  B       b200    t200
550  T       t201    o b77 b200  T       t201    o b29 b200
551  B       b201    t201  B       b201    t201
552  T       t202    o b75 b201  T       t202    o b27 b201
553  B       b202    t202  B       b202    t202
554  T       t203    o b73 b202  T       t203    o b25 b202
555  B       b203    t203  B       b203    t203
556  T       t204    o b71 b203  T       t204    o b23 b203
557  B       b204    t204  B       b204    t204
558  T       t205    o b69 b204  T       t205    o b21 b204
559  B       b205    t205  B       b205    t205
560  T       t206    o b67 b205  T       t206    o b19 b205
561  B       b206    t206  B       b206    t206
562  T       t207    o b65 b206  T       t207    o b17 b206
563  B       b207    t207  B       b207    t207
564  T       t208    o b63 b207  T       t208    o b15 b207
565  B       b208    t208  B       b208    t208
566  T       t209    o b61 b208  T       t209    o b13 b208
567  B       b209    t209  B       b209    t209
568  T       t210    o b59 b209  T       t210    o b11 b209
569  B       b210    t210  B       b210    t210
570  T       t211    o b57 b210  T       t211    o b9 b210
571  B       b211    t211  B       b211    t211
572  T       t212    o b55 b211  T       t212    o b7 b211
573  B       b212    t212  B       b212    t212
574  T       t213    o b53 b212  T       t213    o b5 b212
575  B       b213    t213  B       b213    t213
576  T       t214    o b51 b213  NSummary!resource       resource        resource Summary
577  B       b214    t214  P       p213    String auto
578  T       t215    o b49 b214  O       o213    resource p213
579  B       b215    t215  NOcaml  Ocaml   Ocaml NIL
580  T       t216    o b47 b215  NOcaml!type_lid type_lid        type_lid Ocaml
581    P       p214    Number 2332
582    P       p215    Number 2341
583    O       o215    type_lid p214 p215
584    P       p216    String auto_info
585    O       o216    type_lid p216
586    T       t216    o216
587  B       b216    t216  B       b216    t216
588  T       t217    o b45 b216  T       t217    o215 b216
589  B       b217    t217  B       b217    t217
590  T       t218    o b43 b217  NOcaml!type_prod        type_prod       type_prod Ocaml
591  B       b218    t218  P       p217    Number 2343
592  T       t219    o b41 b218  P       p218    Number 2367
593  B       b219    t219  O       o218    type_prod p217 p218
594  T       t220    o b39 b219  P       p219    Number 2349
595    O       o219    type_lid p217 p219
596    P       p220    String tactic
597    O       o220    type_lid p220
598    T       t220    o220
599  B       b220    t220  B       b220    t220
600  T       t221    o b37 b220  T       t221    o219 b220
601  B       b221    t221  B       b221    t221
602  T       t222    o b35 b221  P       p221    Number 2352
603    P       p222    Number 2358
604    O       o222    type_lid p221 p222
605    T       t222    o222 b220
606  B       b222    t222  B       b222    t222
607  T       t223    o b33 b222  P       p223    Number 2361
608    O       o223    type_lid p223 p218
609    T       t223    o223 b220
610  B       b223    t223  B       b223    t223
611  T       t224    o b31 b223  T       t224    o b223 b4
612  B       b224    t224  B       b224    t224
613  T       t225    o b29 b224  T       t225    o b222 b224
614  B       b225    t225  B       b225    t225
615  T       t226    o b27 b225  T       t226    o b221 b225
616  B       b226    t226  B       b226    t226
617  T       t227    o b25 b226  T       t227    o218 b226
618  B       b227    t227  B       b227    t227
619  T       t228    o b23 b227  T       t228    o213 b217 b227
620  B       b228    t228  B       b228    t228
621  T       t229    o b21 b228  P       p228    String cache
622  B       b229    t229  O       o228    resource p228
623  NSummary!resource       resource        resource Summary  P       p229    Number 1424
624  P       p237    String auto  P       p230    Number 1434
625  O       o237    resource p237  O       o230    type_lid p229 p230
626  NOcaml  Ocaml   Ocaml NIL  P       p231    String cache_rule
627  NOcaml!type_lid type_lid        type_lid Ocaml  O       o231    type_lid p231
628  P       p238    Number 2332  T       t231    o231
629  P       p239    Number 2341  B       b231    t231
630  O       o239    type_lid p238 p239  T       t232    o230 b231
631  P       p240    String auto_info  B       b232    t232
632    P       p232    Number 1436
633    P       p233    Number 1441
634    O       o233    type_lid p232 p233
635    O       o234    type_lid p228
636    T       t234    o234
637    B       b234    t234
638    T       t235    o233 b234
639    B       b235    t235
640    T       t236    o228 b232 b235
641    B       b236    t236
642    P       p236    String elim
643    O       o236    resource p236
644    P       p237    Number 1761
645    P       p238    Number 1783
646    O       o238    type_prod p237 p238
647    P       p239    Number 1765
648    O       o239    type_lid p237 p239
649    P       p240    String term
650  O       o240    type_lid p240  O       o240    type_lid p240
651  T       t240    o240  T       t240    o240
652  B       b240    t240  B       b240    t240
653  T       t241    o239 b240  T       t241    o239 b240
654  B       b241    t241  B       b241    t241
655  NOcaml!type_prod        type_prod       type_prod Ocaml  NOcaml!type_fun type_fun        type_fun Ocaml
656  P       p241    Number 2343  P       p241    Number 1769
657  P       p242    Number 2367  P       p242    Number 1782
658  O       o242    type_prod p241 p242  O       o242    type_fun p241 p242
659  P       p243    Number 2349  P       p243    Number 1772
660  O       o243    type_lid p241 p243  O       o243    type_lid p241 p243
661  P       p244    String tactic  P       p244    String int
662  O       o244    type_lid p244  O       o244    type_lid p244
663  T       t244    o244  T       t244    o244
664  B       b244    t244  B       b244    t244
665  T       t245    o243 b244  T       t245    o243 b244
666  B       b245    t245  B       b245    t245
667  P       p245    Number 2352  P       p245    Number 1776
668  P       p246    Number 2358  O       o245    type_lid p245 p242
669  O       o246    type_lid p245 p246  T       t246    o245 b220
 T       t246    o246 b244  
670  B       b246    t246  B       b246    t246
671  P       p247    Number 2361  T       t247    o242 b245 b246
 O       o247    type_lid p247 p242  
 T       t247    o247 b244  
672  B       b247    t247  B       b247    t247
673  T       t248    o b247 b4  T       t248    o b247 b4
674  B       b248    t248  B       b248    t248
675  T       t249    o b246 b248  T       t249    o b241 b248
676  B       b249    t249  B       b249    t249
677  T       t250    o b245 b249  T       t250    o238 b249
678  B       b250    t250  B       b250    t250
679  T       t251    o242 b250  P       p250    Number 1785
680  B       b251    t251  P       p251    Number 1798
681  T       t252    o237 b241 b251  O       o251    type_fun p250 p251
682    P       p252    Number 1788
683    O       o252    type_lid p250 p252
684    T       t252    o252 b244
685  B       b252    t252  B       b252    t252
686  P       p252    String cache  P       p253    Number 1792
687  O       o252    resource p252  O       o253    type_lid p253 p251
688  P       p253    Number 1424  T       t253    o253 b220
689  P       p254    Number 1434  B       b253    t253
690  O       o254    type_lid p253 p254  T       t254    o251 b252 b253
691  P       p255    String cache_rule  B       b254    t254
692  O       o255    type_lid p255  T       t255    o236 b250 b254
 T       t255    o255  
693  B       b255    t255  B       b255    t255
694  T       t256    o254 b255  P       p255    String eqcd
695  B       b256    t256  O       o255    resource p255
696  P       p256    Number 1436  P       p256    Number 6168
697  P       p257    Number 1441  P       p257    Number 6181
698  O       o257    type_lid p256 p257  O       o257    type_prod p256 p257
699  O       o258    type_lid p252  P       p258    Number 6172
700  T       t258    o258  O       o258    type_lid p256 p258
701    T       t258    o258 b240
702  B       b258    t258  B       b258    t258
703  T       t259    o257 b258  P       p259    Number 6175
704    O       o259    type_lid p259 p257
705    T       t259    o259 b220
706  B       b259    t259  B       b259    t259
707  T       t260    o252 b256 b259  T       t260    o b259 b4
708  B       b260    t260  B       b260    t260
709  P       p260    String elim  T       t261    o b258 b260
710  O       o260    resource p260  B       b261    t261
711  P       p261    Number 1761  T       t262    o257 b261
712  P       p262    Number 1783  B       b262    t262
713  O       o262    type_prod p261 p262  P       p262    Number 6183
714  P       p263    Number 1765  P       p263    Number 6189
715  O       o263    type_lid p261 p263  O       o263    type_lid p262 p263
716  P       p264    String term  T       t263    o263 b220
717  O       o264    type_lid p264  B       b263    t263
718  T       t264    o264  T       t264    o255 b262 b263
719  B       b264    t264  B       b264    t264
720  T       t265    o263 b264  P       p264    String intro
721  B       b265    t265  O       o264    resource p264
722  NOcaml!type_fun type_fun        type_fun Ocaml  P       p265    Number 1815
723  P       p265    Number 1769  P       p266    Number 1852
724  P       p266    Number 1782  O       o266    type_prod p265 p266
725  O       o266    type_fun p265 p266  P       p267    Number 1819
 P       p267    Number 1772  
726  O       o267    type_lid p265 p267  O       o267    type_lid p265 p267
727  P       p268    String int  T       t267    o267 b240
728  O       o268    type_lid p268  B       b267    t267
729  T       t268    o268  P       p268    Number 1823
730  B       b268    t268  P       p269    Number 1851
731  T       t269    o267 b268  O       o269    type_prod p268 p269
732  B       b269    t269  P       p270    Number 1829
733  P       p269    Number 1776  O       o270    type_lid p268 p270
734  O       o269    type_lid p269 p266  P       p271    String string
735  T       t270    o269 b244  O       o271    type_lid p271
736  B       b270    t270  T       t271    o271
 T       t271    o266 b269 b270  
737  B       b271    t271  B       b271    t271
738  T       t272    o b271 b4  T       t272    o270 b271
739  B       b272    t272  B       b272    t272
740  T       t273    o b265 b272  NOcaml!type_apply       type_apply      type_apply Ocaml
741  B       b273    t273  P       p272    Number 1832
742  T       t274    o262 b273  P       p273    Number 1842
743  B       b274    t274  O       o273    type_apply p272 p273
744  P       p274    Number 1785  P       p274    Number 1836
745  P       p275    Number 1798  O       o274    type_lid p274 p273
746  O       o275    type_fun p274 p275  P       p275    String option
747  P       p276    Number 1788  O       o275    type_lid p275
748  O       o276    type_lid p274 p276  T       t275    o275
749  T       t276    o276 b268  B       b275    t275
750    T       t276    o274 b275
751  B       b276    t276  B       b276    t276
752  P       p277    Number 1792  P       p276    Number 1835
753  O       o277    type_lid p277 p275  O       o276    type_lid p272 p276
754  T       t277    o277 b244  T       t277    o276 b244
755  B       b277    t277  B       b277    t277
756  T       t278    o275 b276 b277  T       t278    o273 b276 b277
757  B       b278    t278  B       b278    t278
758  T       t279    o260 b274 b278  P       p278    Number 1845
759    O       o278    type_lid p278 p269
760    T       t279    o278 b220
761  B       b279    t279  B       b279    t279
762  P       p279    String eqcd  T       t280    o b279 b4
763  O       o279    resource p279  B       b280    t280
764  P       p280    Number 6168  T       t281    o b278 b280
765  P       p281    Number 6181  B       b281    t281
766  O       o281    type_prod p280 p281  T       t282    o b272 b281
 P       p282    Number 6172  
 O       o282    type_lid p280 p282  
 T       t282    o282 b264  
767  B       b282    t282  B       b282    t282
768  P       p283    Number 6175  T       t283    o269 b282
 O       o283    type_lid p283 p281  
 T       t283    o283 b244  
769  B       b283    t283  B       b283    t283
770  T       t284    o b283 b4  T       t284    o b283 b4
771  B       b284    t284  B       b284    t284
772  T       t285    o b282 b284  T       t285    o b267 b284
773  B       b285    t285  B       b285    t285
774  T       t286    o281 b285  T       t286    o266 b285
775  B       b286    t286  B       b286    t286
776  P       p286    Number 6183  P       p286    Number 1854
777  P       p287    Number 6189  P       p287    Number 1860
778  O       o287    type_lid p286 p287  O       o287    type_lid p286 p287
779  T       t287    o287 b244  T       t287    o287 b220
780  B       b287    t287  B       b287    t287
781  T       t288    o279 b286 b287  T       t288    o264 b286 b287
782  B       b288    t288  B       b288    t288
783  P       p288    String intro  P       p288    String reduce
784  O       o288    resource p288  O       o288    resource p288
785  P       p289    Number 1815  P       p289    Number 2920
786  P       p290    Number 1852  P       p290    Number 2931
787  O       o290    type_prod p289 p290  O       o290    type_prod p289 p290
788  P       p291    Number 1819  P       p291    Number 2924
789  O       o291    type_lid p289 p291  O       o291    type_lid p289 p291
790  T       t291    o291 b264  T       t291    o291 b240
791  B       b291    t291  B       b291    t291
792  P       p292    Number 1823  P       p292    Number 2927
793  P       p293    Number 1851  O       o292    type_lid p292 p290
794  O       o293    type_prod p292 p293  P       p293    String conv
795  P       p294    Number 1829  O       o293    type_lid p293
796  O       o294    type_lid p292 p294  T       t293    o293
797  P       p295    String string  B       b293    t293
798  O       o295    type_lid p295  T       t294    o292 b293
799  T       t295    o295  B       b294    t294
800    T       t295    o b294 b4
801  B       b295    t295  B       b295    t295
802  T       t296    o294 b295  T       t296    o b291 b295
803  B       b296    t296  B       b296    t296
804  NOcaml!type_apply       type_apply      type_apply Ocaml  T       t297    o290 b296
805  P       p296    Number 1832  B       b297    t297
806  P       p297    Number 1842  P       p297    Number 2933
807  O       o297    type_apply p296 p297  P       p298    Number 2937
808  P       p298    Number 1836  O       o298    type_lid p297 p298
809  O       o298    type_lid p298 p297  T       t298    o298 b293
810  P       p299    String option  B       b298    t298
811  O       o299    type_lid p299  T       t299    o288 b297 b298
 T       t299    o299  
812  B       b299    t299  B       b299    t299
813  T       t300    o298 b299  P       p299    String squash
814  B       b300    t300  O       o299    resource p299
815  P       p300    Number 1835  P       p300    Number 4017
816  O       o300    type_lid p296 p300  P       p301    Number 4028
817  T       t301    o300 b268  O       o301    type_lid p300 p301
818  B       b301    t301  P       p302    String squash_info
819  T       t302    o297 b300 b301  O       o302    type_lid p302
820    T       t302    o302
821  B       b302    t302  B       b302    t302
822  P       p302    Number 1845  T       t303    o301 b302
 O       o302    type_lid p302 p293  
 T       t303    o302 b244  
823  B       b303    t303  B       b303    t303
824  T       t304    o b303 b4  P       p303    Number 4030
825  B       b304    t304  P       p304    Number 4043
826  T       t305    o b302 b304  O       o304    type_fun p303 p304
827    P       p305    Number 4033
828    O       o305    type_lid p303 p305
829    T       t305    o305 b244
830  B       b305    t305  B       b305    t305
831  T       t306    o b296 b305  P       p306    Number 4037
832    O       o306    type_lid p306 p304
833    T       t306    o306 b220
834  B       b306    t306  B       b306    t306
835  T       t307    o293 b306  T       t307    o304 b305 b306
836  B       b307    t307  B       b307    t307
837  T       t308    o b307 b4  T       t308    o299 b303 b307
838  B       b308    t308  B       b308    t308
839  T       t309    o b291 b308  P       p308    String sub
840  B       b309    t309  O       o308    resource p308
841  T       t310    o290 b309  P       p309    Number 4882
842  B       b310    t310  P       p310    Number 4899
843  P       p310    Number 1854  O       o310    type_lid p309 p310
844  P       p311    Number 1860  P       p311    String sub_resource_info
845  O       o311    type_lid p310 p311  O       o311    type_lid p311
846  T       t311    o311 b244  T       t311    o311
847  B       b311    t311  B       b311    t311
848  T       t312    o288 b310 b311  T       t312    o310 b311
849  B       b312    t312  B       b312    t312
850  P       p312    String reduce  P       p312    Number 4901
851  O       o312    resource p312  P       p313    Number 4907
852  P       p313    Number 2920  O       o313    type_lid p312 p313
853  P       p314    Number 2931  T       t313    o313 b220
854  O       o314    type_prod p313 p314  B       b313    t313
855  P       p315    Number 2924  T       t314    o308 b312 b313
856  O       o315    type_lid p313 p315  B       b314    t314
857  T       t315    o315 b264  P       p314    String toploop
858  B       b315    t315  O       o314    resource p314
859  P       p316    Number 2927  P       p315    Number 2445
860  O       o316    type_lid p316 p314  P       p316    Number 2467
861  P       p317    String conv  O       o316    type_prod p315 p316
862  O       o317    type_lid p317  P       p317    Number 2451
863  T       t317    o317  O       o317    type_lid p315 p317
864    T       t317    o317 b271
865  B       b317    t317  B       b317    t317
866  T       t318    o316 b317  P       p318    Number 2454
867  B       b318    t318  P       p319    Number 2460
868  T       t319    o b318 b4  O       o319    type_lid p318 p319
869    T       t319    o319 b271
870  B       b319    t319  B       b319    t319
871  T       t320    o b315 b319  P       p320    Number 2463
872  B       b320    t320  O       o320    type_lid p320 p316
873  T       t321    o314 b320  P       p321    String expr
874    O       o321    type_lid p321
875    T       t321    o321
876  B       b321    t321  B       b321    t321
877  P       p321    Number 2933  T       t322    o320 b321
 P       p322    Number 2937  
 O       o322    type_lid p321 p322  
 T       t322    o322 b317  
878  B       b322    t322  B       b322    t322
879  T       t323    o312 b321 b322  T       t323    o b322 b4
880  B       b323    t323  B       b323    t323
881  P       p323    String squash  T       t324    o b319 b323
882  O       o323    resource p323  B       b324    t324
883  P       p324    Number 4017  T       t325    o b317 b324
884  P       p325    Number 4028  B       b325    t325
885  O       o325    type_lid p324 p325  T       t326    o316 b325
 P       p326    String squash_info  
 O       o326    type_lid p326  
 T       t326    o326  
886  B       b326    t326  B       b326    t326
887  T       t327    o325 b326  P       p326    Number 2469
888  B       b327    t327  P       p327    Number 2478
889  P       p327    Number 4030  O       o327    type_lid p326 p327
890  P       p328    Number 4043  P       p328    String top_table
891  O       o328    type_fun p327 p328  O       o328    type_lid p328
892  P       p329    Number 4033  T       t328    o328
893  O       o329    type_lid p327 p329  B       b328    t328
894  T       t329    o329 b268  T       t329    o327 b328
895  B       b329    t329  B       b329    t329
896  P       p330    Number 4037  T       t330    o314 b326 b329
 O       o330    type_lid p330 p328  
 T       t330    o330 b244  
897  B       b330    t330  B       b330    t330
898  T       t331    o328 b329 b330  P       p330    String typeinf
899  B       b331    t331  O       o330    resource p330
900  T       t332    o323 b327 b331  P       p331    Number 2151
901  B       b332    t332  P       p332    Number 2172
902  P       p332    String sub  O       o332    type_lid p331 p332
903  O       o332    resource p332  P       p333    String typeinf_resource_info
904  P       p333    Number 4882  O       o333    type_lid p333
905  P       p334    Number 4899  T       t333    o333
906  O       o334    type_lid p333 p334  B       b333    t333
907  P       p335    String sub_resource_info  T       t334    o332 b333
908  O       o335    type_lid p335  B       b334    t334
909  T       t335    o335  P       p334    Number 2174
910  B       b335    t335  P       p335    Number 2186
911  T       t336    o334 b335  O       o335    type_lid p334 p335
912    P       p336    String typeinf_func
913    O       o336    type_lid p336
914    T       t336    o336
915  B       b336    t336  B       b336    t336
916  P       p336    Number 4901  T       t337    o335 b336
 P       p337    Number 4907  
 O       o337    type_lid p336 p337  
 T       t337    o337 b244  
917  B       b337    t337  B       b337    t337
918  T       t338    o332 b336 b337  T       t338    o330 b334 b337
919  B       b338    t338  B       b338    t338
920  P       p338    String toploop  P       p338    String typeinf_subst
921  O       o338    resource p338  O       o338    resource p338
922  P       p339    Number 2445  P       p339    Number 1825
923  P       p340    Number 2467  P       p340    Number 1843
924  O       o340    type_prod p339 p340  O       o340    type_lid p339 p340
925  P       p341    Number 2451  P       p341    String typeinf_subst_info
926  O       o341    type_lid p339 p341  O       o341    type_lid p341
927  T       t341    o341 b295  T       t341    o341
928  B       b341    t341  B       b341    t341
929  P       p342    Number 2454  T       t342    o340 b341
930  P       p343    Number 2460  B       b342    t342
931  O       o343    type_lid p342 p343  P       p342    Number 1862
932  T       t343    o343 b295  O       o342    type_lid p278 p342
933    P       p343    String typeinf_subst_fun
934    O       o343    type_lid p343
935    T       t343    o343
936  B       b343    t343  B       b343    t343
937  P       p344    Number 2463  T       t344    o342 b343
938  O       o344    type_lid p344 p340  B       b344    t344
939  P       p345    String expr  T       t345    o338 b342 b344
 O       o345    type_lid p345  
 T       t345    o345  
940  B       b345    t345  B       b345    t345
941  T       t346    o344 b345  T       t346    o b345 b4
942  B       b346    t346  B       b346    t346
943  T       t347    o b346 b4  T       t347    o b338 b346
944  B       b347    t347  B       b347    t347
945  T       t348    o b343 b347  T       t348    o b330 b347
946  B       b348    t348  B       b348    t348
947  T       t349    o b341 b348  T       t349    o b314 b348
948  B       b349    t349  B       b349    t349
949  T       t350    o340 b349  T       t350    o b308 b349
950  B       b350    t350  B       b350    t350
951  P       p350    Number 2469  T       t351    o b299 b350
952  P       p351    Number 2478  B       b351    t351
953  O       o351    type_lid p350 p351  T       t352    o b288 b351
 P       p352    String top_table  
 O       o352    type_lid p352  
 T       t352    o352  
954  B       b352    t352  B       b352    t352
955  T       t353    o351 b352  T       t353    o b264 b352
956  B       b353    t353  B       b353    t353
957  T       t354    o338 b350 b353  T       t354    o b255 b353
958  B       b354    t354  B       b354    t354
959  P       p354    String typeinf  T       t355    o b236 b354
960  O       o354    resource p354  B       b355    t355
961  P       p355    Number 2151  T       t356    o b228 b355
962  P       p356    Number 2172  B       b356    t356
963  O       o356    type_lid p355 p356  T       t357    o2 b5 b213 b356
 P       p357    String typeinf_resource_info  
 O       o357    type_lid p357  
 T       t357    o357  
964  B       b357    t357  B       b357    t357
965  T       t358    o356 b357  T       t358    o1 b357
966  B       b358    t358  B       b358    t358
967  P       p358    Number 2174  P       p358    Number 20
968  P       p359    Number 2186  P       p359    Number 42
969  O       o359    type_lid p358 p359  O       o359    location p358 p359
970  P       p360    String typeinf_func  P       p360    String Czf_itt_member
971  O       o360    type_lid p360  O       o360    parent p360
972  T       t360    o360  T       t360    o360
973  B       b360    t360  B       b360    t360
974  T       t361    o359 b360  T       t361    o b360 b4
975  B       b361    t361  B       b361    t361
976  T       t362    o354 b358 b361  P       p361    String Czf_itt_eq
977    O       o361    parent p361
978    T       t362    o361
979  B       b362    t362  B       b362    t362
980  P       p362    String typeinf_subst  T       t363    o b362 b4
981  O       o362    resource p362  B       b363    t363
982  P       p363    Number 1825  T       t364    o b363 b4
983  P       p364    Number 1843  B       b364    t364
984  O       o364    type_lid p363 p364  T       t365    o b361 b364
 P       p365    String typeinf_subst_info  
 O       o365    type_lid p365  
 T       t365    o365  
985  B       b365    t365  B       b365    t365
986  T       t366    o364 b365  T       t366    o2 b361 b365 b356
987  B       b366    t366  B       b366    t366
988  P       p366    Number 1862  T       t367    o359 b366
 O       o366    type_lid p302 p366  
 P       p367    String typeinf_subst_fun  
 O       o367    type_lid p367  
 T       t367    o367  
989  B       b367    t367  B       b367    t367
990  T       t368    o366 b367  P       p367    Number 43
991  B       b368    t368  P       p368    Number 64
992  T       t369    o362 b366 b368  O       o368    location p367 p368
993    P       p369    String Czf_itt_group
994    O       o369    parent p369
995    T       t369    o369
996  B       b369    t369  B       b369    t369
997  T       t370    o b369 b4  T       t370    o b369 b4
998  B       b370    t370  B       b370    t370
999  T       t371    o b362 b370  P       p370    String Czf_itt_equiv
1000    O       o370    parent p370
1001    T       t371    o370
1002  B       b371    t371  B       b371    t371
1003  T       t372    o b354 b371  T       t372    o b371 b4
1004  B       b372    t372  B       b372    t372
1005  T       t373    o b338 b372  P       p372    String Czf_itt_pair
1006    O       o372    parent p372
1007    T       t373    o372
1008  B       b373    t373  B       b373    t373
1009  T       t374    o b332 b373  T       t374    o b373 b4
1010  B       b374    t374  B       b374    t374
1011  T       t375    o b323 b374  P       p374    String Czf_itt_singleton
1012    O       o374    parent p374
1013    T       t375    o374
1014  B       b375    t375  B       b375    t375
1015  T       t376    o b312 b375  T       t376    o b375 b4
1016  B       b376    t376  B       b376    t376
1017  T       t377    o b288 b376  P       p376    String Czf_itt_union
1018    O       o376    parent p376
1019    T       t377    o376
1020  B       b377    t377  B       b377    t377
1021  T       t378    o b279 b377  T       t378    o b377 b4
1022  B       b378    t378  B       b378    t378
1023  T       t379    o b260 b378  P       p378    String Czf_itt_subset
1024    O       o378    parent p378
1025    T       t379    o378
1026  B       b379    t379  B       b379    t379
1027  T       t380    o b252 b379  T       t380    o b379 b4
1028  B       b380    t380  B       b380    t380
1029  T       t230    o2 b21 b229 b380  P       p380    String Czf_itt_dexists
1030  B       b230    t230  O       o380    parent p380
1031  T       t231    o8 b230  T       t381    o380
 B       b231    t231  
 P       p231    Number 20  
 P       p232    Number 42  
 O       o232    location p231 p232  
 T       t232    o b19 b4  
 B       b232    t232  
 T       t233    o b17 b232  
 B       b233    t233  
 T       t234    o2 b17 b233 b380  
 B       b234    t234  
 T       t235    o232 b234  
 B       b235    t235  
 P       p383    Number 43  
 P       p235    Number 64  
 O       o235    location p383 p235  
 T       t236    o b254 b4  
 B       b236    t236  
 T       t237    o b239 b236  
 B       b237    t237  
 T       t242    o b15 b237  
 B       b242    t242  
 T       t243    o b13 b242  
 B       b243    t243  
 T       t381    o b11 b243  
1032  B       b381    t381  B       b381    t381
1033  T       t382    o b9 b381  T       t382    o b381 b4
1034  B       b382    t382  B       b382    t382
1035  T       t423    o b7 b382  P       p382    String Czf_itt_and
1036  B       b423    t423  O       o382    parent p382
1037  T       t435    o b5 b423  T       t383    o382
1038    B       b383    t383
1039    T       t384    o b383 b4
1040    B       b384    t384
1041    P       p384    String Czf_itt_dall
1042    O       o384    parent p384
1043    T       t385    o384
1044    B       b385    t385
1045    T       t386    o b385 b4
1046    B       b386    t386
1047    P       p386    String Czf_itt_set_ind
1048    O       o386    parent p386
1049    T       t387    o386
1050    B       b387    t387
1051    T       t388    o b387 b4
1052    B       b388    t388
1053    P       p388    String Czf_itt_all
1054    O       o388    parent p388
1055    T       t389    o388
1056    B       b389    t389
1057    T       t390    o b389 b4
1058    B       b390    t390
1059    P       p390    String Czf_itt_sep
1060    O       o390    parent p390
1061    T       t391    o390
1062    B       b391    t391
1063    T       t392    o b391 b4
1064    B       b392    t392
1065    P       p392    String Itt_record_label0
1066    O       o392    parent p392
1067    T       t393    o392
1068    B       b393    t393
1069    T       t394    o b393 b4
1070    B       b394    t394
1071    P       p394    String Itt_nat
1072    O       o394    parent p394
1073    T       t395    o394
1074    B       b395    t395
1075    T       t396    o b395 b4
1076    B       b396    t396
1077    T       t397    o b396 b4
1078    B       b397    t397
1079    T       t398    o b394 b397
1080    B       b398    t398
1081    T       t399    o b392 b398
1082    B       b399    t399
1083    T       t400    o b390 b399
1084    B       b400    t400
1085    T       t401    o b388 b400
1086    B       b401    t401
1087    T       t402    o b386 b401
1088    B       b402    t402
1089    T       t403    o b384 b402
1090    B       b403    t403
1091    T       t404    o b382 b403
1092    B       b404    t404
1093    T       t405    o b380 b404
1094    B       b405    t405
1095    T       t406    o b378 b405
1096    B       b406    t406
1097    T       t407    o b376 b406
1098    B       b407    t407
1099    T       t408    o b374 b407
1100    B       b408    t408
1101    T       t409    o b372 b408
1102    B       b409    t409
1103    T       t410    o b370 b409
1104    B       b410    t410
1105    T       t411    o2 b370 b410 b356
1106    B       b411    t411
1107    T       t412    o368 b411
1108    B       b412    t412
1109    P       p412    Number 65
1110    P       p413    Number 86
1111    O       o413    location p412 p413
1112    T       t413    o2 b372 b4 b356
1113    B       b413    t413
1114    T       t414    o413 b413
1115    B       b414    t414
1116    P       p414    Number 88
1117    P       p415    Number 99
1118    O       o415    location p414 p415
1119    NSummary!summary_item   summary_item    summary_item Summary
1120    O       o416    summary_item
1121    NOcaml!str_open str_open        str_open Ocaml
1122    O       o417    str_open p414 p415
1123    NOcaml!string   string  string Ocaml
1124    P       p417    String Printf
1125    O       o418    string p417
1126    T       t418    o418
1127    B       b418    t418
1128    T       t419    o b418 b4
1129    B       b419    t419
1130    T       t420    o417 b419
1131    B       b420    t420
1132    T       t421    o416 b420
1133    B       b421    t421
1134    T       t422    o415 b421
1135    B       b422    t422
1136    P       p422    Number 100
1137    P       p423    Number 113
1138    O       o423    location p422 p423
1139    O       o424    str_open p422 p423
1140    P       p424    String Mp_debug
1141    O       o425    string p424
1142    T       t425    o425
1143    B       b425    t425
1144    T       t426    o b425 b4
1145    B       b426    t426
1146    T       t427    o424 b426
1147    B       b427    t427
1148    T       t428    o416 b427
1149    B       b428    t428
1150    T       t429    o423 b428
1151    B       b429    t429
1152    P       p429    Number 114
1153    P       p430    Number 143
1154    O       o430    location p429 p430
1155    O       o431    str_open p429 p430
1156    P       p431    String Refiner
1157    O       o432    string p431
1158    T       t432    o432
1159    B       b432    t432
1160    P       p432    String TermType
1161    O       o433    string p432
1162    T       t433    o433
1163    B       b433    t433
1164    T       t434    o b433 b4
1165    B       b434    t434
1166    T       t435    o b432 b434
1167  B       b435    t435  B       b435    t435
1168  T       t436    o2 b5 b435 b380  T       t436    o b432 b435
1169  B       b436    t436  B       b436    t436
1170  T       t437    o235 b436  T       t437    o431 b436
1171  B       b437    t437  B       b437    t437
1172  P       p437    Number 65  T       t438    o416 b437
1173  P       p438    Number 86  B       b438    t438
1174  O       o438    location p437 p438  T       t439    o430 b438
1175  P       p439    String Czf_itt_equiv  B       b439    t439
1176  O       o441    parent p439  P       p439    Number 144
1177  T       t441    o441  P       p440    Number 169
1178  B       b441    t441  O       o440    location p439 p440
1179  T       t442    o b441 b4  O       o441    str_open p439 p440
1180    P       p441    String Term
1181    O       o442    string p441
1182    T       t442    o442
1183  B       b442    t442  B       b442    t442
1184  P       p442    String Czf_itt_pair  T       t443    o b442 b4
 O       o442    parent p442  
 T       t443    o442  
1185  B       b443    t443  B       b443    t443
1186  T       t444    o b443 b4  T       t444    o b432 b443
1187  B       b444    t444  B       b444    t444
1188  P       p444    String Czf_itt_singleton  T       t445    o b432 b444
 O       o444    parent p444  
 T       t445    o444  
1189  B       b445    t445  B       b445    t445
1190  T       t446    o b445 b4  T       t446    o441 b445
1191  B       b446    t446  B       b446    t446
1192  P       p446    String Czf_itt_union  T       t447    o416 b446
 O       o446    parent p446  
 T       t447    o446  
1193  B       b447    t447  B       b447    t447
1194  T       t452    o b447 b4  T       t448    o440 b447
1195    B       b448    t448
1196    P       p448    Number 170
1197    P       p449    Number 197
1198    O       o449    location p448 p449
1199    O       o450    str_open p448 p449
1200    P       p450    String TermOp
1201    O       o451    string p450
1202    T       t451    o451
1203    B       b451    t451
1204    T       t452    o b451 b4
1205  B       b452    t452  B       b452    t452
1206  P       p452    String Czf_itt_subset  T       t453    o b432 b452
 O       o452    parent p452  
 T       t453    o452  
1207  B       b453    t453  B       b453    t453
1208  T       t454    o b453 b4  T       t454    o b432 b453
1209  B       b454    t454  B       b454    t454
1210  P       p454    String Czf_itt_dexists  T       t455    o450 b454
 O       o454    parent p454  
 T       t455    o454  
1211  B       b455    t455  B       b455    t455
1212  T       t456    o b455 b4  T       t456    o416 b455
1213  B       b456    t456  B       b456    t456
1214  T       t457    o b456 b4  T       t457    o449 b456
1215  B       b457    t457  B       b457    t457
1216  T       t461    o b454 b457  P       p457    Number 198
1217    P       p458    Number 227
1218    O       o458    location p457 p458
1219    O       o459    str_open p457 p458
1220    P       p459    String TermAddr
1221    O       o460    string p459
1222    T       t460    o460
1223    B       b460    t460
1224    T       t461    o b460 b4
1225  B       b461    t461  B       b461    t461
1226  T       t462    o b452 b461  T       t462    o b432 b461
1227  B       b462    t462  B       b462    t462
1228  T       t463    o b446 b462  T       t463    o b432 b462
1229  B       b463    t463  B       b463    t463
1230  T       t464    o b444 b463  T       t464    o459 b463
1231  B       b464    t464  B       b464    t464
1232  T       t465    o b442 b464  T       t465    o416 b464
1233  B       b465    t465  B       b465    t465
1234  T       t466    o2 b442 b465 b380  T       t466    o458 b465
1235  B       b466    t466  B       b466    t466
1236  T       t467    o438 b466  P       p466    Number 228
1237  B       b467    t467  P       p467    Number 256
1238  P       p467    Number 88  O       o467    location p466 p467
1239  P       p471    Number 99  O       o468    str_open p466 p467
1240  O       o472    location p467 p471  P       p468    String TermMan
1241  NSummary!summary_item   summary_item    summary_item Summary  O       o469    string p468
1242  O       o384    summary_item  T       t469    o469
1243  NOcaml!str_open str_open        str_open Ocaml  B       b469    t469
1244  O       o473    str_open p467 p471  T       t470    o b469 b4
1245  NOcaml!string   string  string Ocaml  B       b470    t470
1246  P       p473    String Printf  T       t471    o b432 b470
1247  O       o474    string p473  B       b471    t471
1248  T       t475    o474  T       t472    o b432 b471
1249    B       b472    t472
1250    T       t473    o468 b472
1251    B       b473    t473
1252    T       t474    o416 b473
1253    B       b474    t474
1254    T       t475    o467 b474
1255  B       b475    t475  B       b475    t475
1256  T       t476    o b475 b4  P       p475    Number 257
1257  B       b476    t476  P       p476    Number 287
1258  T       t488    o473 b476  O       o476    location p475 p476
1259    O       o477    str_open p475 p476
1260    P       p477    String TermSubst
1261    O       o478    string p477
1262    T       t478    o478
1263    B       b478    t478
1264    T       t479    o b478 b4
1265    B       b479    t479
1266    T       t480    o b432 b479
1267    B       b480    t480
1268    T       t481    o b432 b480
1269    B       b481    t481
1270    T       t482    o477 b481
1271    B       b482    t482
1272    T       t483    o416 b482
1273    B       b483    t483
1274    T       t484    o476 b483
1275    B       b484    t484
1276    P       p484    Number 288
1277    P       p485    Number 315
1278    O       o485    location p484 p485
1279    O       o486    str_open p484 p485
1280    P       p486    String Refine
1281    O       o487    string p486
1282    T       t487    o487
1283    B       b487    t487
1284    T       t488    o b487 b4
1285  B       b488    t488  B       b488    t488
1286  T       t489    o384 b488  T       t489    o b432 b488
1287  B       b489    t489  B       b489    t489
1288  T       t517    o472 b489  T       t490    o b432 b489
1289  B       b518    t517  B       b490    t490
1290  P       p520    Number 100  T       t491    o486 b490
1291  P       p385    String Refiner  B       b491    t491
1292  O       o386    string p385  T       t492    o416 b491
1293  T       t386    o386  B       b492    t492
1294  B       b386    t386  T       t493    o485 b492
1295  O       o401    string p145  B       b493    t493
1296  T       t401    o401  P       p493    Number 316
1297  B       b401    t401  P       p494    Number 348
1298  T       t402    o b401 b4  O       o494    location p493 p494
1299  B       b402    t402  O       o495    str_open p493 p494
1300  O       o408    string p135  P       p495    String RefineError
1301  T       t408    o408  O       o496    string p495
1302  B       b408    t408  T       t496    o496
1303  T       t409    o b408 b4  B       b496    t496
1304  B       b409    t409  T       t497    o b496 b4
1305  O       o415    string p137  B       b497    t497
1306  T       t415    o415  T       t498    o b432 b497
1307  B       b415    t415  B       b498    t498
1308  T       t416    o b415 b4  T       t499    o b432 b498
1309  B       b416    t416  B       b499    t499
1310  P       p419    Number 113  T       t500    o495 b499
1311  O       o520    location p520 p419  B       b500    t500
1312  O       o521    str_open p520 p419  T       t501    o416 b500
1313  P       p521    String Mp_debug  B       b501    t501
1314  O       o522    string p521  T       t502    o494 b501
1315  T       t534    o522  B       b502    t502
1316  B       b534    t534  P       p502    Number 349
1317  T       t535    o b534 b4  P       p503    Number 365
1318    O       o503    location p502 p503
1319    O       o504    str_open p502 p503
1320    P       p504    String Mp_resource
1321    O       o505    string p504
1322    T       t505    o505
1323    B       b505    t505
1324    T       t506    o b505 b4
1325    B       b506    t506
1326    T       t507    o504 b506
1327    B       b507    t507
1328    T       t508    o416 b507
1329    B       b508    t508
1330    T       t509    o503 b508
1331    B       b509    t509
1332    P       p509    Number 367
1333    P       p510    Number 383
1334    O       o510    location p509 p510
1335    O       o511    str_open p509 p510
1336    P       p511    String Tactic_type
1337    O       o512    string p511
1338    T       t512    o512
1339    B       b512    t512
1340    T       t513    o b512 b4
1341    B       b513    t513
1342    T       t514    o511 b513
1343    B       b514    t514
1344    T       t515    o416 b514
1345    B       b515    t515
1346    T       t516    o510 b515
1347    B       b516    t516
1348    P       p516    Number 384
1349    P       p517    Number 410
1350    O       o517    location p516 p517
1351    O       o518    str_open p516 p517
1352    P       p518    String Tacticals
1353    O       o519    string p518
1354    T       t519    o519
1355    B       b519    t519
1356    T       t520    o b519 b4
1357    B       b520    t520
1358    T       t521    o b512 b520
1359    B       b521    t521
1360    T       t522    o518 b521
1361    B       b522    t522
1362    T       t523    o416 b522
1363    B       b523    t523
1364    T       t524    o517 b523
1365    B       b524    t524
1366    P       p524    Number 411
1367    P       p525    Number 435
1368    O       o525    location p524 p525
1369    O       o526    str_open p524 p525
1370    P       p526    String Sequent
1371    O       o527    string p526
1372    T       t527    o527
1373    B       b527    t527
1374    T       t528    o b527 b4
1375    B       b528    t528
1376    T       t529    o b512 b528
1377    B       b529    t529
1378    T       t530    o526 b529
1379    B       b530    t530
1380    T       t531    o416 b530
1381    B       b531    t531
1382    T       t532    o525 b531
1383    B       b532    t532
1384    P       p532    Number 436
1385    P       p533    Number 466
1386    O       o533    location p532 p533
1387    O       o534    str_open p532 p533
1388    P       p534    String Conversionals
1389    O       o535    string p534
1390    T       t535    o535
1391  B       b535    t535  B       b535    t535
1392  T       t536    o521 b535  T       t536    o b535 b4
1393  B       b536    t536  B       b536    t536
1394  T       t537    o384 b536  T       t537    o b512 b536
1395  B       b537    t537  B       b537    t537
1396  T       t538    o520 b537  T       t538    o534 b537
1397  B       b538    t538  B       b538    t538
1398  P       p538    Number 114  T       t539    o416 b538
1399  P       p539    Number 143  B       b539    t539
1400  O       o539    location p538 p539  T       t540    o533 b539
1401  O       o540    str_open p538 p539  B       b540    t540
1402  P       p540    String TermType  P       p540    Number 467
1403  O       o541    string p540  P       p541    Number 477
1404  T       t541    o541  O       o541    location p540 p541
1405  B       b541    t541  O       o542    str_open p540 p541
1406  T       t542    o b541 b4  O       o543    string p131
1407  B       b542    t542  T       t543    o543
 T       t543    o b386 b542  
1408  B       b543    t543  B       b543    t543
1409  T       t544    o b386 b543  T       t544    o b543 b4
1410  B       b544    t544  B       b544    t544
1411  T       t545    o540 b544  T       t545    o542 b544
1412  B       b545    t545  B       b545    t545
1413  T       t546    o384 b545  T       t546    o416 b545
1414  B       b546    t546  B       b546    t546
1415  T       t547    o539 b546  T       t547    o541 b546
1416  B       b547    t547  B       b547    t547
1417  P       p547    Number 144  P       p547    Number 478
1418  P       p548    Number 169  P       p548    Number 486
1419  O       o548    location p547 p548  O       o548    location p547 p548
1420  O       o549    str_open p547 p548  O       o549    str_open p547 p548
1421  P       p549    String Term  O       o550    string p129
 O       o550    string p549  
1422  T       t550    o550  T       t550    o550
1423  B       b550    t550  B       b550    t550
1424  T       t551    o b550 b4  T       t551    o b550 b4
1425  B       b551    t551  B       b551    t551
1426  T       t552    o b386 b551  T       t552    o549 b551
1427  B       b552    t552  B       b552    t552
1428  T       t553    o b386 b552  T       t553    o416 b552
1429  B       b553    t553  B       b553    t553
1430  T       t554    o549 b553  T       t554    o548 b553
1431  B       b554    t554  B       b554    t554
1432  T       t555    o384 b554  P       p554    Number 488
1433  B       b555    t555  P       p555    Number 505
1434  T       t556    o548 b555  O       o555    location p554 p555
1435  B       b556    t556  O       o556    str_open p554 p555
1436  P       p556    Number 170  O       o557    string p119
1437  P       p557    Number 197  T       t557    o557
1438  O       o557    location p556 p557  B       b557    t557
1439  O       o558    str_open p556 p557  T       t558    o b557 b4
1440  P       p558    String TermOp  B       b558    t558
1441  O       o559    string p558  T       t559    o556 b558
 T       t559    o559  
1442  B       b559    t559  B       b559    t559
1443  T       t560    o b559 b4  T       t560    o416 b559
1444  B       b560    t560  B       b560    t560
1445  T       t561    o b386 b560  T       t561    o555 b560
1446  B       b561    t561  B       b561    t561
1447  T       t562    o b386 b561  P       p561    Number 506
1448  B       b562    t562  P       p562    Number 527
1449  T       t563    o558 b562  O       o562    location p561 p562
1450  B       b563    t563  O       o563    str_open p561 p562
1451  T       t564    o384 b563  O       o564    string p121
1452    T       t564    o564
1453  B       b564    t564  B       b564    t564
1454  T       t565    o557 b564  T       t565    o b564 b4
1455  B       b565    t565  B       b565    t565
1456  P       p565    Number 198  T       t566    o563 b565
1457  P       p566    Number 227  B       b566    t566
1458  O       o566    location p565 p566  T       t567    o416 b566
1459  O       o567    str_open p565 p566  B       b567    t567
1460  P       p567    String TermAddr  T       t568    o562 b567
 O       o568    string p567  
 T       t568    o568  
1461  B       b568    t568  B       b568    t568
1462  T       t569    o b568 b4  P       p568    Number 529
1463  B       b569    t569  P       p569    Number 545
1464  T       t570    o b386 b569  O       o569    location p568 p569
1465  B       b570    t570  NSummary!opname opname  opname Summary
1466  T       t571    o b386 b570  P       p570    String abel
1467  B       b571    t571  O       o570    opname p570
1468  T       t572    o567 b571  NCzf_itt_abel_group     Czf_itt_abel_group      Czf_itt_abel_group NIL
1469    NCzf_itt_abel_group!abel        abel    abel Czf_itt_abel_group
1470    O       o571    abel
1471    Nvar    var     var NIL
1472    P       p571    Var g
1473    O       o572    var p571
1474    T       t572    o572
1475  B       b572    t572  B       b572    t572
1476  T       t573    o384 b572  T       t573    o571 b572
1477  B       b573    t573  B       b573    t573
1478  T       t574    o566 b573  T       t574    o570 b573
1479  B       b574    t574  B       b574    t574
1480  P       p574    Number 228  T       t575    o569 b574
1481  P       p575    Number 256  B       b575    t575
1482  O       o575    location p574 p575  P       p575    Number 547
1483  O       o576    str_open p574 p575  P       p576    Number 722
1484  P       p576    String TermMan  O       o576    location p575 p576
1485  O       o577    string p576  NSummary!rewrite        rewrite rewrite Summary
1486  T       t577    o577  P       p577    String unfold_abel
1487  B       b577    t577  O       o577    rewrite p577
1488  T       t578    o b577 b4  NItt_logic      Itt_logic       Itt_logic NIL
1489  B       b578    t578  NItt_logic!and  and     and Itt_logic
1490  T       t579    o b386 b578  O       o578    and
1491    NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL
1492    NCzf_itt_group!group    group   group Czf_itt_group
1493    O       o579    group
1494    T       t579    o579 b572
1495  B       b579    t579  B       b579    t579
1496  T       t580    o b386 b579  NItt_logic!all  all     all Itt_logic
1497  B       b580    t580  O       o580    all
1498  T       t581    o576 b580  NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL
1499    NCzf_itt_set!set        set     set Czf_itt_set
1500    O       o581    set
1501    T       t581    o581
1502  B       b581    t581  B       b581    t581
1503  T       t582    o384 b581  NItt_logic!implies      implies implies Itt_logic
1504  B       b582    t582  O       o582    implies
1505  T       t583    o575 b582  NCzf_itt_member Czf_itt_member  Czf_itt_member NIL
1506  B       b583    t583  NCzf_itt_member!mem     mem     mem Czf_itt_member
1507  P       p583    Number 257  O       o583    mem
1508  P       p584    Number 287  P       p583    Var a
1509  O       o584    location p583 p584  O       o584    var p583
1510  O       o585    str_open p583 p584  T       t584    o584
1511  P       p585    String TermSubst  B       b584    t584
1512  O       o586    string p585  NCzf_itt_group!car      car     car Czf_itt_group
1513  T       t586    o586  O       o585    car
1514    T       t585    o585 b572
1515    B       b585    t585
1516    T       t586    o583 b584 b585
1517  B       b586    t586  B       b586    t586
1518  T       t587    o b586 b4  P       p586    Var b
1519    O       o586    var p586
1520    T       t587    o586
1521  B       b587    t587  B       b587    t587
1522  T       t588    o b386 b587  T       t588    o583 b587 b585
1523  B       b588    t588  B       b588    t588
1524  T       t589    o b386 b588  NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL
1525    NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv
1526    O       o588    equiv
1527    NCzf_itt_group!eqG      eqG     eqG Czf_itt_group
1528    O       o589    eqG
1529    T       t589    o589 b572
1530  B       b589    t589  B       b589    t589
1531  T       t590    o585 b589  NCzf_itt_group!op       op      op Czf_itt_group
1532    O       o590    op
1533    T       t590    o590 b572 b584 b587
1534  B       b590    t590  B       b590    t590
1535  T       t591    o384 b590  T       t591    o590 b572 b587 b584
1536  B       b591    t591  B       b591    t591
1537  T       t592    o584 b591  T       t592    o588 b585 b589 b590 b591
1538  B       b592    t592  B       b592    t592
1539  P       p592    Number 288  T       t593    o582 b588 b592
1540  P       p593    Number 315  B       b593    t593
1541  O       o593    location p592 p593  T       t594    o582 b586 b593
1542  O       o594    str_open p592 p593  B       b594    t594 b
1543  P       p594    String Refine  T       t595    o580 b581 b594
1544  O       o595    string p594  B       b595    t595 a
1545  T       t595    o595  T       t596    o580 b581 b595
 B       b595    t595  
 T       t596    o b595 b4  
1546  B       b596    t596  B       b596    t596
1547  T       t597    o b386 b596  T       t597    o578 b579 b596
1548  B       b597    t597  B       b597    t597
1549  T       t598    o b386 b597  NSummary!prim   prim    prim Summary
1550    O       o597    prim
1551    T       t598    o597 b4
1552  B       b598    t598  B       b598    t598
1553  T       t599    o594 b598  T       t599    o577 b573 b597 b598 b4
1554  B       b599    t599  B       b599    t599
1555  T       t600    o384 b599  T       t600    o576 b599
1556  B       b600    t600  B       b600    t600
1557  T       t601    o593 b600  P       p600    Number 724
1558  B       b601    t601  P       p601    Number 796
1559  P       p601    Number 316  O       o601    location p600 p601
1560  P       p602    Number 348  NSummary!dform  dform   dform Summary
1561  O       o602    location p601 p602  P       p602    String abel_df
1562  O       o603    str_open p601 p602  O       o602    dform p602
1563  P       p603    String RefineError  NSummary!except_mode_df except_mode_df  except_mode_df Summary
1564  O       o604    string p603  P       p603    String src
1565  T       t604    o604  O       o603    except_mode_df p603
1566    T       t603    o603
1567    B       b603    t603
1568    T       t604    o b603 b4
1569  B       b604    t604  B       b604    t604
1570  T       t605    o b604 b4  NSummary!df_term        df_term df_term Summary
1571    O       o604    df_term
1572    NPerv!string    string604       string Perv
1573    P       p604    String abel(
1574    O       o605    string604 p604
1575    T       t605    o605
1576  B       b605    t605  B       b605    t605
1577  T       t606    o b386 b605  Nslot   slot    slot NIL
1578    O       o606    slot
1579    T       t606    o606 b572
1580  B       b606    t606  B       b606    t606
1581  T       t607    o b386 b606  P       p606    String )
1582    O       o607    string604 p606
1583    T       t607    o607
1584  B       b607    t607  B       b607    t607
1585  T       t608    o603 b607  T       t608    o b607 b4
1586  B       b608    t608  B       b608    t608
1587  T       t609    o384 b608  T       t609    o b606 b608
1588  B       b609    t609  B       b609    t609
1589  T       t610    o602 b609  T       t610    o b605 b609
1590  B       b610    t610  B       b610    t610
1591  P       p610    Number 349  T       t611    o604 b610
1592  P       p611    Number 365  B       b611    t611
1593  O       o611    location p610 p611  T       t612    o602 b604 b573 b611
1594  O       o612    str_open p610 p611  B       b612    t612
1595  P       p612    String Mp_resource  T       t613    o601 b612
 O       o613    string p612  
 T       t613    o613  
1596  B       b613    t613  B       b613    t613
1597  T       t614    o b613 b4  O       o613    location p p
1598  B       b614    t614  NSummary!rule   rule    rule Summary
1599  T       t615    o612 b614  P       p613    String abel_type
1600    O       o614    rule p613
1601    NSummary!context_param  context_param   context_param Summary
1602    P       p614    String H
1603    O       o615    context_param p614
1604    T       t615    o615
1605  B       b615    t615  B       b615    t615
1606  T       t616    o384 b615  T       t616    o b615 b4
1607  B       b616    t616  B       b616    t616
1608  T       t617    o611 b616  NSummary!meta_implies   meta_implies    meta_implies Summary
1609  B       b617    t617  O       o616    meta_implies
1610  P       p617    Number 367  NSummary!meta_theorem   meta_theorem    meta_theorem Summary
1611  P       p618    Number 383  O       o617    meta_theorem
1612  O       o618    location p617 p618  NBase_trivial   Base_trivial    Base_trivial NIL
1613  O       o619    str_open p617 p618  NBase_trivial!squash    squash  squash Base_trivial
1614  P       p619    String Tactic_type  O       o618    squash
1615  O       o620    string p619  T       t618    o618
1616    B       b618    t618
1617    T       t619    o b618 b4
1618    C       h       H
1619    NItt_equal      Itt_equal       Itt_equal NIL
1620    NItt_equal!equal        equal   equal Itt_equal
1621    O       o619    equal
1622    NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL
1623    NItt_record_label0!label        label   label Itt_record_label0
1624    O       o620    label
1625  T       t620    o620  T       t620    o620
1626  B       b620    t620  B       b620    t620
1627  T       t621    o b620 b4  T       t621    o619 b620 b572 b572
1628  B       b621    t621  S       s       t619 h
1629  T       t622    o619 b621  G       s       t621
1630    B       b621    s
1631    T       t622    o617 b621
1632  B       b622    t622  B       b622    t622
1633  T       t623    o384 b622  P       p622    Var ext
1634    O       o622    var p622
1635    T       t623    o622
1636  B       b623    t623  B       b623    t623
1637  T       t624    o618 b623  T       t624    o b623 b4
1638  B       b624    t624  NItt_equal!type type    type Itt_equal
1639  P       p624    Number 384  O       o624    type
1640  P       p625    Number 410  T       t625    o624 b573
1641  O       o625    location p624 p625  S       s625    t624 h
1642  O       o626    str_open p624 p625  G       s625    t625
1643  P       p626    String Tacticals  B       b625    s625
1644  O       o627    string p626  T       t626    o617 b625
1645  T       t627    o627  B       b626    t626
1646    T       t627    o616 b622 b626
1647  B       b627    t627  B       b627    t627
1648  T       t628    o b627 b4  NSummary!interactive    interactive     interactive Summary
1649  B       b628    t628  O       o627    interactive
1650  T       t629    o b620 b628  NSummary!ext_rule       ext_rule        ext_rule Summary
1651    P       p627    String "rwh unfold_abel 0 thenT autoT thenT rwh fold_isset 0 ttca"
1652    O       o628    ext_rule p627
1653    NSummary!status_incomplete      status_incomplete       status_incomplete Summary
1654    O       o629    status_incomplete
1655    T       t629    o629
1656  B       b629    t629  B       b629    t629
1657  T       t630    o626 b629  NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary
1658  B       b630    t630  O       o630    ext_unjustified
1659  T       t631    o384 b630  NSummary!tactic_arg     tactic_arg      tactic_arg Summary
1660  B       b631    t631  P       p630    String main
1661  T       t632    o625 b631  O       o631    tactic_arg p630
1662    NSummary!msequent       msequent        msequent Summary
1663    O       o632    msequent
1664    T       t632    o b621 b4
1665  B       b632    t632  B       b632    t632
1666  P       p632    Number 411  T       t633    o632 b625 b632
1667  P       p633    Number 435  B       b633    t633
1668  O       o633    location p632 p633  NSummary!parent_none    parent_none     parent_none Summary
1669  O       o634    str_open p632 p633  O       o633    parent_none
1670  P       p634    String Sequent  T       t634    o633
1671  O       o635    string p634  B       b634    t634
1672  T       t635    o635  T       t635    o631 b633 b4 b634
1673  B       b635    t635  B       b635    t635
1674  T       t636    o b635 b4  T       t636    o630 b635 b4
1675  B       b636    t636  B       b636    t636
1676  T       t637    o b620 b636  T       t637    o628 b629 b636 b4 b4
1677  B       b637    t637  B       b637    t637
1678  T       t638    o634 b637  T       t638    o627 b637
1679  B       b638    t638  B       b638    t638
1680  T       t639    o384 b638  NSummary!resource_defs  resource_defs   resource_defs Summary
1681  B       b639    t639  P       p638    Number 823
1682  T       t640    o633 b639  P       p639    Number 831
1683  B       b640    t640  O       o639    resource_defs p638 p639 p264
1684  P       p640    Number 436  NOcaml!uid      uid     uid Ocaml
1685  P       p641    Number 466  P       p640    Number 829
1686  O       o641    location p640 p641  O       o640    uid p640 p639
1687  O       o642    str_open p640 p641  P       p641    String []
1688  P       p642    String Conversionals  O       o641    uid p641
1689  O       o643    string p642  T       t641    o641
1690  T       t643    o643  B       b641    t641
1691    T       t642    o640 b641
1692    B       b642    t642
1693    T       t643    o b642 b4
1694  B       b643    t643  B       b643    t643
1695  T       t644    o b643 b4  T       t644    o639 b643
1696  B       b644    t644  B       b644    t644
1697  T       t645    o b620 b644  T       t645    o b644 b4
1698  B       b645    t645  B       b645    t645
1699  T       t646    o642 b645  T       t646    o614 b616 b627 b638 b645
1700  B       b646    t646  B       b646    t646
1701  T       t647    o384 b646  T       t647    o613 b646
1702  B       b647    t647  B       b647    t647
1703  T       t648    o641 b647  P       p647    String abel_intro
1704  B       b648    t648  O       o647    rule p647
1705  P       p648    Number 467  S       s647    t624 h
1706  P       p649    Number 477  G       s647    t579
1707  O       o649    location p648 p649  B       b648    s647
1708  O       o650    str_open p648 p649  T       t648    o617 b648
1709  O       o651    string p147  B       b649    t648
1710  T       t651    o651  H       h649    a t581
1711  B       b651    t651  H       h650    b t581
1712  T       t652    o b651 b4  H       h651    x t586
1713  B       b652    t652  H       h652    y t588
1714  T       t653    o650 b652  S       s652    t624 h h649 h650 h651 h652
1715  B       b653    t653  G       s652    t592
1716  T       t654    o384 b653  B       b652    s652
1717  B       b654    t654  T       t652    o617 b652
1718  T       t655    o649 b654  B       b653    t652
1719  B       b655    t655  S       s653    t624 h
1720  P       p655    Number 478  G       s653    t573
1721  P       p656    Number 486  B       b654    s653
1722  O       o656    location p655 p656  T       t654    o617 b654
1723  O       o657    str_open p655 p656  B       b655    t654
1724  T       t657    o657 b402  T       t655    o616 b653 b655
1725  B       b657    t657  B       b656    t655
1726  T       t658    o384 b657  T       t656    o616 b649 b656
1727  B       b658    t658  B       b657    t656
1728  T       t659    o656 b658  T       t657    o616 b622 b657
1729  B       b659    t659  B       b658    t657
1730  P       p659    Number 488  P       p658    String "rwh unfold_abel 0 thenT autoT"
1731  P       p660    Number 505  O       o658    ext_rule p658
1732  O       o660    location p659 p660  T       t658    o b652 b4
1733  O       o661    str_open p659 p660  B       b659    t658
1734  T       t661    o661 b409  T       t659    o b648 b659
1735  B       b661    t661  B       b660    t659
1736  T       t662    o384 b661  T       t660    o b621 b660
1737  B       b662    t662  B       b661    t660
1738  T       t663    o660 b662  T       t661    o632 b654 b661
1739  B       b663    t663  B       b662    t661
1740  P       p663    Number 506  T       t662    o631 b662 b4 b634
1741  P       p664    Number 527  B       b663    t662
1742  O       o664    location p663 p664  T       t663    o630 b663 b4
1743  O       o665    str_open p663 p664  B       b664    t663
1744  T       t665    o665 b416  T       t664    o658 b629 b664 b4 b4
1745  B       b665    t665  B       b665    t664
1746  T       t666    o384 b665  T       t665    o627 b665
1747  B       b666    t666  B       b666    t665
1748  T       t667    o664 b666  P       p666    Number 958
1749  B       b667    t667  P       p667    Number 965
1750  P       p667    Number 529  O       o667    resource_defs p666 p667 p264
1751  P       p668    Number 549  P       p668    Number 963
1752  O       o668    location p667 p668  O       o668    uid p668 p667
1753  NSummary!opname opname  opname Summary  T       t668    o668 b641
1754  P       p469    String abel  B       b668    t668
1755  O       o469    opname p469  T       t669    o b668 b4
 NCzf_itt_abel_group     Czf_itt_abel_group      Czf_itt_abel_group NIL  
 NCzf_itt_abel_group!abel        abel    abel Czf_itt_abel_group  
 O       o470    abel  
 NSummary!rule   rule    rule Summary  
 NSummary!context_param  context_param   context_param Summary  
 P       p422    String H  
 O       o422    context_param p422  
 T       t422    o422  
 B       b422    t422  
 NSummary!meta_implies   meta_implies    meta_implies Summary  
 O       o423    meta_implies  
 NSummary!meta_theorem   meta_theorem    meta_theorem Summary  
 O       o424    meta_theorem  
 NBase_trivial   Base_trivial    Base_trivial NIL  
 NBase_trivial!squash    squash  squash Base_trivial  
 O       o425    squash  
 T       t425    o425  
 B       b425    t425  
 T       t426    o b425 b4  
 C       h       H  
 NCzf_itt_set    Czf_itt_set     Czf_itt_set NIL  
 NCzf_itt_set!isset      isset   isset Czf_itt_set  
 O       o426    isset  
 Nvar    var     var NIL  
 P       p470    Var g  
 O       o471    var p470  
 T       t471    o471  
 B       b471    t471  
 P       p669    Var r  
 O       o669    var p669  
 T       t669    o669  
1756  B       b669    t669  B       b669    t669
1757  T       t670    o470 b471 b669  T       t670    o667 b669
1758  B       b670    t670  B       b670    t670
1759  T       t671    o469 b670  T       t671    o b670 b4
1760  B       b671    t671  B       b671    t671
1761  T       t672    o668 b671  T       t672    o647 b616 b658 b666 b671
1762  B       b672    t672  B       b672    t672
1763  P       p672    Number 551  T       t673    o613 b672
1764  P       p673    Number 758  B       b673    t673
1765  O       o673    location p672 p673  NSummary!id     id      id Summary
1766  NSummary!rewrite        rewrite rewrite Summary  P       p673    Number 206743266
1767  P       p674    String unfold_abel  O       o673    id p673
1768  O       o674    rewrite p674  T       t674    o673
1769  NItt_logic      Itt_logic       Itt_logic NIL  B       b674    t674
1770  NItt_logic!and  and     and Itt_logic  T       t675    o613 b674
1771  O       o675    and  B       b675    t675
1772  NSummary!dform  dform   dform Summary  T       t676    o b675 b4
1773  P       p476    String abel_df  B       b676    t676
1774  O       o476    dform p476  T       t677    o b673 b676
1775  NSummary!except_mode_df except_mode_df  except_mode_df Summary  B       b677    t677
1776  P       p477    String src  T       t678    o b647 b677
 O       o477    except_mode_df p477  
 T       t477    o477  
 B       b477    t477  
 T       t478    o b477 b4  
 B       b478    t478  
 NSummary!df_term        df_term df_term Summary  
 O       o478    df_term  
 NPerv!string    string478       string Perv  
 P       p478    String abel(  
 O       o479    string478 p478  
 T       t479    o479  
 B       b479    t479  
 Nslot   slot    slot NIL  
 O       o480    slot  
 T       t480    o480 b471  
 B       b480    t480  
 P       p480    String )  
 O       o481    string478 p480  
 T       t481    o481  
 B       b481    t481  
 T       t482    o b481 b4  
 B       b482    t482  
 NItt_equal      Itt_equal       Itt_equal NIL  
 NItt_equal!equal        equal494        equal Itt_equal  
 O       o494    equal494  
 NItt_record_label0      Itt_record_label0       Itt_record_label0 NIL  
 NItt_record_label0!label        label   label Itt_record_label0  
 O       o495    label  
 T       t495    o495  
 B       b495    t495  
 T       t496    o494 b495 b471 b471  
 S       s496    t426 h  
 G       s496    t496  
 B       b496    s496  
 T       t497    o424 b496  
 B       b497    t497  
 P       p432    Var ext  
 O       o432    var p432  
 T       t433    o432  
 B       b433    t433  
 T       t434    o b433 b4  
 NCzf_itt_member Czf_itt_member  Czf_itt_member NIL  
 NCzf_itt_member!mem     mem     mem Czf_itt_member  
 O       o434    mem  
 NCzf_itt_group  Czf_itt_group   Czf_itt_group NIL  
 NCzf_itt_group!group    group   group Czf_itt_group  
 O       o497    group  
 T       t498    o497 b471  
 B       b675    t498  
 T       t675    o426 b669  
 B       b676    t675  
 NCzf_itt_equiv  Czf_itt_equiv   Czf_itt_equiv NIL  
 NCzf_itt_equiv!equiv    equiv   equiv Czf_itt_equiv  
 O       o676    equiv  
 S       s498    t434 h  
 G       s498    t498  
 B       b498    s498  
 T       t499    o424 b498  
 B       b499    t499  
 NCzf_itt_group!car      car     car Czf_itt_group  
 O       o435    car  
 T       t500    o435 b471  
 B       b500    t500  
 T       t676    o676 b500 b669  
 B       b677    t676  
 NItt_logic!all  all     all Itt_logic  
 O       o677    all  
 NCzf_itt_set!set        set     set Czf_itt_set  
 O       o678    set  
 T       t678    o678  
1777  B       b678    t678  B       b678    t678
1778  NItt_logic!implies      implies implies Itt_logic  T       t679    o b613 b678
1779  O       o679    implies  B       b679    t679
1780  P       p679    Var a  T       t680    o b600 b679
 O       o680    var p679  
 T       t680    o680  
1781  B       b680    t680  B       b680    t680
1782  T       t681    o434 b680 b500  T       t681    o b575 b680
1783  B       b681    t681  B       b681    t681
1784  P       p681    Var b  T       t682    o b568 b681
 O       o681    var p681  
 T       t682    o681  
1785  B       b682    t682  B       b682    t682
1786  T       t683    o434 b682 b500  T       t683    o b561 b682
1787  B       b683    t683  B       b683    t683
1788  NCzf_itt_group!op       op      op Czf_itt_group  T       t684    o b554 b683
 O       o440    op  
 T       t684    o440 b471 b680 b682  
1789  B       b684    t684  B       b684    t684
1790  T       t685    o440 b471 b682 b680  T       t685    o b547 b684
1791  B       b685    t685  B       b685    t685
1792  T       t686    o676 b500 b669 b684 b685  T       t686    o b540 b685
1793  B       b686    t686  B       b686    t686
1794  T       t687    o679 b683 b686  T       t687    o b532 b686
1795  B       b687    t687  B       b687    t687
1796  T       t688    o679 b681 b687  T       t688    o b524 b687
1797  B       b688    t688 b  B       b688    t688
1798  T       t689    o677 b678 b688  T       t689    o b516 b688
1799  B       b689    t689 a  B       b689    t689
1800  T       t690    o677 b678 b689  T       t690    o b509 b689
1801  B       b690    t690  B       b690    t690
1802  T       t691    o675 b677 b690  T       t691    o b502 b690
1803  B       b691    t691  B       b691    t691
1804  T       t692    o675 b676 b691  T       t692    o b493 b691
1805  B       b692    t692  B       b692    t692
1806  T       t693    o675 b675 b692  T       t693    o b484 b692
1807  B       b693    t693  B       b693    t693
1808  NSummary!prim   prim    prim Summary  T       t694    o b475 b693
 O       o693    prim  
 T       t694    o693 b4  
1809  B       b694    t694  B       b694    t694
1810  T       t695    o674 b670 b693 b694 b4  T       t695    o b466 b694
1811  B       b695    t695  B       b695    t695
1812  T       t696    o673 b695  T       t696    o b457 b695
1813  B       b696    t696  B       b696    t696
1814  P       p696    Number 760  T       t697    o b448 b696
1815  P       p697    Number 851  B       b697    t697
1816  O       o697    location p696 p697  T       t698    o b439 b697
 P       p698    String "; "  
 O       o698    string478 p698  
 T       t698    o698  
1817  B       b698    t698  B       b698    t698
1818  T       t699    o480 b669  T       t699    o b429 b698
1819  B       b699    t699  B       b699    t699
1820  T       t700    o b699 b482  T       t700    o b422 b699
1821  B       b700    t700  B       b700    t700
1822  T       t701    o b698 b700  T       t701    o b414 b700
1823  B       b701    t701  B       b701    t701
1824  T       t702    o b480 b701  T       t702    o b412 b701
1825  B       b702    t702  B       b702    t702
1826  T       t703    o b479 b702  T       t703    o b367 b702
1827  B       b703    t703  B       b703    t703
1828  T       t704    o478 b703  T       t704    o b358 b703
 B       b704    t704  
 T       t705    o476 b478 b670 b704  
 B       b705    t705  
 T       t706    o697 b705  
 B       b706    t706  
 P       p706    Number 853  
 P       p707    Number 1075  
 O       o707    location p706 p707  
 P       p708    String abel_type  
 O       o708    rule p708  
 T       t708    o b422 b4  
 B       b708    t708  
 S       s708    t426 h  
 G       s708    t675  
 B       b709    s708  
 T       t709    o424 b709  
 B       b710    t709  
 NItt_equal!type type    type Itt_equal  
 O       o710    type  
 T       t710    o710 b670  
 S       s710    t434 h  
 G       s710    t710  
 B       b711    s710  
 T       t711    o424 b711  
 B       b712    t711  
 T       t712    o423 b499 b712  
 B       b713    t712  
 T       t713    o423 b710 b713  
 B       b714    t713  
 T       t714    o423 b497 b714  
 B       b715    t714  
 NSummary!interactive    interactive     interactive Summary  
 O       o715    interactive  
 NSummary!ext_rule       ext_rule        ext_rule Summary  
 P       p715    String "rwh unfold_abel 0 thenT autoT thenT rwh fold_isset 0 ttca"  
 O       o716    ext_rule p715  
 NSummary!status_incomplete      status_incomplete       status_incomplete Summary  
 O       o717    status_incomplete  
 T       t717    o717  
 B       b717    t717  
 NSummary!ext_unjustified        ext_unjustified ext_unjustified Summary  
 O       o718    ext_unjustified  
 NSummary!tactic_arg     tactic_arg      tactic_arg Summary  
 P       p718    String main  
 O       o719    tactic_arg p718  
 NSummary!msequent       msequent        msequent Summary  
 O       o720    msequent  
 T       t720    o b498 b4  
 B       b720    t720  
 T       t721    o b709 b720  
 B       b721    t721  
 T       t722    o b496 b721  
 B       b722    t722  
 T       t723    o720 b711 b722  
 B       b723    t723  
 NSummary!parent_none    parent_none     parent_none Summary  
 O       o723    parent_none  
 T       t724    o723  
 B       b724    t724  
 T       t725    o719 b723 b4 b724  
 B       b725    t725  
 T       t726    o718 b725 b4  
 B       b726    t726  
 T       t727    o716 b717 b726 b4 b4  
 B       b727    t727  
 T       t728    o715 b727  
 B       b728    t728  
 NSummary!resource_defs  resource_defs   resource_defs Summary  
 P       p728    Number 878  
 P       p729    Number 886  
 O       o729    resource_defs p728 p729 p288  
 NOcaml!uid      uid     uid Ocaml  
 P       p730    Number 884  
 O       o730    uid p730 p729  
 P       p451    String []  
 O       o451    uid p451  
 T       t451    o451  
 B       b451    t451  
 T       t730    o730 b451  
 B       b730    t730  
 T       t731    o b730 b4  
 B       b731    t731  
 T       t732    o729 b731  
 B       b732    t732  
 T       t733    o b732 b4  
 B       b733    t733  
 T       t734    o708 b708 b715 b728 b733  
 B       b734    t734  
 T       t735    o707 b734  
 B       b735    t735  
 P       p735    Number 1077  
 P       p736    Number 1483  
 O       o736    location p735 p736  
 P       p737    String abel_intro  
 O       o737    rule p737  
 S       s737    t434 h  
 G       s737    t676  
 B       b737    s737  
 T       t737    o424 b737  
 B       b738    t737  
 H       h738    a t678  
 H       h739    b t678  
 H       h740    x t681  
 H       h741    y t683  
 S       s741    t434 h h738 h739 h740 h741  
 G       s741    t686  
 B       b741    s741  
 T       t741    o424 b741  
 B       b742    t741  
 S       s742    t434 h  
 G       s742    t670  
 B       b743    s742  
 T       t743    o424 b743  
 B       b744    t743  
 T       t744    o423 b742 b744  
 B       b745    t744  
 T       t745    o423 b738 b745  
 B       b746    t745  
 T       t746    o423 b710 b746  
 B       b747    t746  
 T       t747    o423 b499 b747  
 B       b748    t747  
 T       t748    o423 b497 b748  
 B       b749    t748  
 P       p749    String "rwh unfold_abel 0 thenT autoT"  
 O       o749    ext_rule p749  
 T       t749    o b741 b4  
 B       b750    t749  
 T       t750    o b737 b750  
 B       b751    t750  
 T       t751    o b709 b751  
 B       b752    t751  
 T       t752    o b498 b752  
 B       b753    t752  
 T       t753    o b496 b753  
 B       b754    t753  
 T       t754    o720 b743 b754  
 B       b755    t754  
 T       t755    o719 b755 b4 b724  
 B       b756    t755  
 S       s756    t434 h  
 G       s756    t675  
 B       b757    s756  
 T       t757    o720 b757 b754  
 B       b758    t757  
 S       s758    t434 h  
 G       s758    t692  
 B       b759    s758  
 T       t759    o720 b759 b754  
 B       b760    t759  
 NSummary!arg_named      arg_named       arg_named Summary  
 P       p760    String d_auto  
 O       o760    arg_named p760  
 NSummary!arg_bool       arg_bool        arg_bool Summary  
 P       p761    String true  
 O       o761    arg_bool p761  
 T       t761    o761  
 B       b761    t761  
 T       t762    o760 b761  
 B       b762    t762  
 T       t763    o b762 b4  
 B       b763    t763  
 S       s763    t434 h  
 G       s763    t693  
 B       b764    s763  
 T       t764    o720 b764 b754  
 B       b765    t764  
 T       t765    o2 b756  
 B       b766    t765  
 T       t766    o719 b765 b763 b766  
 B       b767    t766  
 T       t767    o2 b767  
 B       b768    t767  
 T       t768    o719 b760 b763 b768  
 B       b769    t768  
 T       t769    o2 b769  
 B       b770    t769  
 T       t770    o719 b758 b4 b770  
 B       b771    t770  
 T       t771    o b771 b4  
 B       b772    t771  
 T       t772    o718 b756 b772  
 B       b773    t772  
 P       p773    String "rwh unfold_isset 0 thenT autoT thenT rwh fold_isset 0 thenT autoT"  
 O       o773    ext_rule p773  
 T       t773    o718 b771 b4  
 B       b774    t773  
 T       t774    o773 b717 b774 b4 b4  
 B       b775    t774  
 T       t775    o b775 b4  
 B       b776    t775  
 T       t776    o749 b717 b773 b776 b4  
 B       b777    t776  
 T       t777    o715 b777  
 B       b778    t777  
 P       p778    Number 1103  
 P       p779    Number 1110  
 O       o779    resource_defs p778 p779 p288  
 P       p780    Number 1108  
 O       o780    uid p780 p779  
 T       t780    o780 b451  
 B       b780    t780  
 T       t781    o b780 b4  
 B       b781    t781  
 T       t782    o779 b781  
 B       b782    t782  
 T       t783    o b782 b4  
 B       b783    t783  
 T       t784    o737 b708 b749 b778 b783  
 B       b784    t784  
 T       t785    o736 b784  
 B       b785    t785  
 O       o457    location p p  
 NSummary!id     id      id Summary  
 P       p457    Number 206743266  
 O       o458    id p457  
 T       t458    o458  
 B       b458    t458  
 T       t459    o457 b458  
 B       b459    t459  
 T       t460    o b459 b4  
 B       b460    t460  
 T       t786    o b785 b460  
 B       b786    t786  
 T       t787    o b735 b786  
 B       b787    t787  
 T       t788    o b706 b787  
 B       b788    t788  
 T       t789    o b696 b788  
 B       b789    t789  
 T       t790    o b672 b789  
 B       b790    t790  
 T       t791    o b667 b790  
 B       b791    t791  
 T       t792    o b663 b791  
 B       b792    t792  
 T       t793    o b659 b792  
 B       b793    t793  
 T       t794    o b655 b793  
 B       b794    t794  
 T       t795    o b648 b794  
 B       b795    t795  
 T       t796    o b640 b795  
 B       b796    t796  
 T       t797    o b632 b796  
 B       b797    t797  
 T       t798    o b624 b797  
 B       b798    t798  
 T       t799    o b617 b798  
 B       b799    t799  
 T       t800    o b610 b799  
 B       b800    t800  
 T       t801    o b601 b800  
 B       b801    t801  
 T       t802    o b592 b801  
 B       b802    t802  
 T       t803    o b583 b802  
 B       b803    t803  
 T       t804    o b574 b803  
 B       b804    t804  
 T       t805    o b565 b804  
 B       b805    t805  
 T       t806    o b556 b805  
 B       b806    t806  
 T       t807    o b547 b806  
 B       b807    t807  
 T       t808    o b538 b807  
 B       b808    t808  
 T       t809    o b518 b808  
 B       b809    t809  
 T       t810    o b467 b809  
 B       b810    t810  
 T       t811    o b437 b810  
 B       b811    t811  
 T       t812    o b235 b811  
 B       b812    t812  
 T       t813    o b231 b812  

Legend:
Removed from v.3554  
changed lines
  Added in v.3555

  ViewVC Help
Powered by ViewVC 1.1.26