|
1 \begin{theindex} |
|
2 |
|
3 \item {\tt[]}, \bold{7} |
|
4 \item {\tt\#}, \bold{7} |
|
5 \item {\ttnot}, \bold{3} |
|
6 \item {\tt-->}, \bold{3} |
|
7 \item {\tt\&}, \bold{3} |
|
8 \item {\ttor}, \bold{3} |
|
9 \item {\tt?}, \bold{3}, 4 |
|
10 \item {\ttall}, \bold{3} |
|
11 \item {\ttuniquex}, \bold{3} |
|
12 \item {\tt *}, \bold{17} |
|
13 \item {\tt +}, \bold{17} |
|
14 \item {\tt -}, \bold{17} |
|
15 \item {\tt <}, \bold{17} |
|
16 \item {\tt <=}, \bold{17} |
|
17 \item \ttlbr, \bold{9} |
|
18 \item \ttrbr, \bold{9} |
|
19 \item {\tt==>}, \bold{9} |
|
20 \item {\tt==}, \bold{18} |
|
21 \item {\tt\%}, \bold{3} |
|
22 \item {\tt =>}, \bold{2} |
|
23 |
|
24 \indexspace |
|
25 |
|
26 \item {\tt addsimps}, \bold{22} |
|
27 \item {\tt Addsplits}, \bold{24} |
|
28 \item {\tt addsplits}, \bold{24} |
|
29 \item {\tt Asm_full_simp_tac}, \bold{21} |
|
30 \item {\tt asm_full_simp_tac}, \bold{22} |
|
31 \item {\tt Asm_simp_tac}, \bold{21} |
|
32 \item {\tt asm_simp_tac}, \bold{22} |
|
33 |
|
34 \indexspace |
|
35 |
|
36 \item {\tt bool}, 2 |
|
37 |
|
38 \indexspace |
|
39 |
|
40 \item {\tt case}, \bold{3}, 4, \bold{13}, 24 |
|
41 \item {\tt constdefs}, \bold{18} |
|
42 \item {\tt consts}, \bold{7} |
|
43 \item {\tt context}, \bold{11} |
|
44 \item current theory, \bold{11} |
|
45 |
|
46 \indexspace |
|
47 |
|
48 \item {\tt datatype}, \bold{7} |
|
49 \item {\tt defs}, \bold{18} |
|
50 \item {\tt delsimps}, \bold{22} |
|
51 \item {\tt Delsplits}, \bold{24} |
|
52 \item {\tt delsplits}, \bold{24} |
|
53 \item {\tt div}, \bold{17} |
|
54 |
|
55 \indexspace |
|
56 |
|
57 \item {\tt exhaust_tac}, \bold{14} |
|
58 |
|
59 \indexspace |
|
60 |
|
61 \item {\tt False}, \bold{3} |
|
62 \item formula, \bold{3} |
|
63 \item {\tt Full_simp_tac}, \bold{21} |
|
64 \item {\tt full_simp_tac}, \bold{22} |
|
65 |
|
66 \indexspace |
|
67 |
|
68 \item {\tt hd}, \bold{12} |
|
69 |
|
70 \indexspace |
|
71 |
|
72 \item {\tt if}, \bold{3}, 4, 24 |
|
73 \item {\tt infixr}, \bold{7} |
|
74 \item inner syntax, \bold{8} |
|
75 |
|
76 \indexspace |
|
77 |
|
78 \item {\tt LEAST}, \bold{17} |
|
79 \item {\tt let}, \bold{3}, 4, 23 |
|
80 \item {\tt list}, 2 |
|
81 \item loading theories, 12 |
|
82 |
|
83 \indexspace |
|
84 |
|
85 \item {\tt Main}, \bold{2} |
|
86 \item measure function, \bold{29} |
|
87 \item {\tt mod}, \bold{17} |
|
88 |
|
89 \indexspace |
|
90 |
|
91 \item {\tt nat}, 2, \bold{17} |
|
92 |
|
93 \indexspace |
|
94 |
|
95 \item parent theory, \bold{1} |
|
96 \item primitive recursion, \bold{13} |
|
97 \item proof scripts, \bold{2} |
|
98 |
|
99 \indexspace |
|
100 |
|
101 \item {\tt recdef}, 29--31 |
|
102 \item reloading theories, 12 |
|
103 |
|
104 \indexspace |
|
105 |
|
106 \item schematic variable, \bold{4} |
|
107 \item {\tt set}, 2 |
|
108 \item {\tt show_brackets}, \bold{4} |
|
109 \item {\tt show_types}, \bold{3}, 11 |
|
110 \item {\tt Simp_tac}, \bold{21} |
|
111 \item {\tt simp_tac}, \bold{22} |
|
112 \item simplifier, \bold{20} |
|
113 \item simpset, \bold{21} |
|
114 |
|
115 \indexspace |
|
116 |
|
117 \item tactic, \bold{11} |
|
118 \item term, \bold{3} |
|
119 \item theory, \bold{1} |
|
120 \item {\tt tl}, \bold{12} |
|
121 \item total, \bold{7} |
|
122 \item tracing the simplifier, \bold{25} |
|
123 \item {\tt True}, \bold{3} |
|
124 \item type constraints, \bold{3} |
|
125 \item type inference, \bold{3} |
|
126 \item type synonyms, \bold{18} |
|
127 \item {\tt types}, \bold{18} |
|
128 |
|
129 \indexspace |
|
130 |
|
131 \item unknown, \bold{4} |
|
132 \item {\tt update}, \bold{12} |
|
133 \item {\tt use_thy}, \bold{2}, 12 |
|
134 |
|
135 \end{theindex} |