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