author | wenzelm |
Thu, 23 Nov 2006 22:38:30 +0100 | |
changeset 21506 | b2a673894ce5 |
parent 19046 | bc5c6c9b114e |
child 22360 | 26ead7ed4f4b |
permissions | -rw-r--r-- |
11658 | 1 |
(* Title: Pure/Isar/induct_attrib.ML |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
4 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
5 |
Declaration of rules for cases and induction. |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
6 |
*) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
7 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
8 |
signature INDUCT_ATTRIB = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
9 |
sig |
11730 | 10 |
val vars_of: term -> term list |
21506 | 11 |
val dest_rules: Proof.context -> |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
12 |
{type_cases: (string * thm) list, set_cases: (string * thm) list, |
18210 | 13 |
type_induct: (string * thm) list, set_induct: (string * thm) list, |
14 |
type_coinduct: (string * thm) list, set_coinduct: (string * thm) list} |
|
21506 | 15 |
val print_rules: Proof.context -> unit |
11730 | 16 |
val lookup_casesT : Proof.context -> string -> thm option |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
17 |
val lookup_casesS : Proof.context -> string -> thm option |
11730 | 18 |
val lookup_inductT : Proof.context -> string -> thm option |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
19 |
val lookup_inductS : Proof.context -> string -> thm option |
18210 | 20 |
val lookup_coinductT : Proof.context -> string -> thm option |
21 |
val lookup_coinductS : Proof.context -> string -> thm option |
|
11730 | 22 |
val find_casesT: Proof.context -> typ -> thm list |
18226 | 23 |
val find_casesS: Proof.context -> term -> thm list |
11730 | 24 |
val find_inductT: Proof.context -> typ -> thm list |
18226 | 25 |
val find_inductS: Proof.context -> term -> thm list |
18210 | 26 |
val find_coinductT: Proof.context -> typ -> thm list |
18226 | 27 |
val find_coinductS: Proof.context -> term -> thm list |
18728 | 28 |
val cases_type: string -> attribute |
29 |
val cases_set: string -> attribute |
|
30 |
val induct_type: string -> attribute |
|
31 |
val induct_set: string -> attribute |
|
32 |
val coinduct_type: string -> attribute |
|
33 |
val coinduct_set: string -> attribute |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
34 |
val casesN: string |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
35 |
val inductN: string |
18210 | 36 |
val coinductN: string |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
37 |
val typeN: string |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
38 |
val setN: string |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
39 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
40 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
41 |
structure InductAttrib: INDUCT_ATTRIB = |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
42 |
struct |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
43 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
44 |
|
11730 | 45 |
(** misc utils **) |
46 |
||
47 |
(* encode_type -- for indexing purposes *) |
|
48 |
||
49 |
fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) |
|
50 |
| encode_type (TFree (a, _)) = Free (a, dummyT) |
|
51 |
| encode_type (TVar (a, _)) = Var (a, dummyT); |
|
52 |
||
53 |
||
54 |
(* variables -- ordered left-to-right, preferring right *) |
|
55 |
||
18210 | 56 |
fun vars_of tm = |
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18977
diff
changeset
|
57 |
rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); |
11730 | 58 |
|
18210 | 59 |
local |
11730 | 60 |
|
61 |
val mk_var = encode_type o #2 o Term.dest_Var; |
|
62 |
||
18210 | 63 |
fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => |
64 |
raise THM ("No variables in conclusion of rule", 0, [thm]); |
|
65 |
||
11730 | 66 |
in |
67 |
||
18210 | 68 |
fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty => |
69 |
raise THM ("No variables in major premise of rule", 0, [thm]); |
|
11730 | 70 |
|
18210 | 71 |
val left_var_concl = concl_var hd; |
72 |
val right_var_concl = concl_var List.last; |
|
11730 | 73 |
|
74 |
end; |
|
75 |
||
76 |
||
77 |
||
18637 | 78 |
(** induct data **) |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
79 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
80 |
(* rules *) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
81 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
82 |
type rules = (string * thm) NetRules.T; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
83 |
|
12381 | 84 |
val init_rules = |
13105
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12381
diff
changeset
|
85 |
NetRules.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso |
3d1e7a199bdc
use eq_thm_prop instead of slightly inadequate eq_thm;
wenzelm
parents:
12381
diff
changeset
|
86 |
Drule.eq_thm_prop (th1, th2)); |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
87 |
|
17184 | 88 |
fun lookup_rule (rs: rules) = AList.lookup (op =) (NetRules.rules rs); |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
89 |
|
18637 | 90 |
fun pretty_rules ctxt kind rs = |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
91 |
let val thms = map snd (NetRules.rules rs) |
18637 | 92 |
in Pretty.big_list kind (map (ProofContext.pretty_thm ctxt) thms) end; |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
93 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
94 |
|
18637 | 95 |
(* context data *) |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
96 |
|
18637 | 97 |
fun dest ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = |
98 |
{type_cases = NetRules.rules casesT, |
|
99 |
set_cases = NetRules.rules casesS, |
|
100 |
type_induct = NetRules.rules inductT, |
|
101 |
set_induct = NetRules.rules inductS, |
|
102 |
type_coinduct = NetRules.rules coinductT, |
|
103 |
set_coinduct = NetRules.rules coinductS}; |
|
104 |
||
105 |
structure Induct = GenericDataFun |
|
106 |
( |
|
18210 | 107 |
val name = "Isar/induct"; |
108 |
type T = (rules * rules) * (rules * rules) * (rules * rules); |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
109 |
|
11730 | 110 |
val empty = |
18210 | 111 |
((init_rules (left_var_prem o #2), init_rules (Thm.major_prem_of o #2)), |
112 |
(init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)), |
|
113 |
(init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2))); |
|
18637 | 114 |
|
16424 | 115 |
val extend = I; |
18637 | 116 |
|
18210 | 117 |
fun merge _ (((casesT1, casesS1), (inductT1, inductS1), (coinductT1, coinductS1)), |
118 |
((casesT2, casesS2), (inductT2, inductS2), (coinductT2, coinductS2))) = |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
119 |
((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)), |
18210 | 120 |
(NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)), |
121 |
(NetRules.merge (coinductT1, coinductT2), NetRules.merge (coinductS1, coinductS2))); |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
122 |
|
18637 | 123 |
fun print generic ((casesT, casesS), (inductT, inductS), (coinductT, coinductS)) = |
124 |
let val ctxt = Context.proof_of generic in |
|
125 |
[pretty_rules ctxt "coinduct type:" coinductT, |
|
126 |
pretty_rules ctxt "coinduct set:" coinductS, |
|
127 |
pretty_rules ctxt "induct type:" inductT, |
|
128 |
pretty_rules ctxt "induct set:" inductS, |
|
129 |
pretty_rules ctxt "cases type:" casesT, |
|
130 |
pretty_rules ctxt "cases set:" casesS] |
|
131 |
|> Pretty.chunks |> Pretty.writeln |
|
132 |
end |
|
133 |
); |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
134 |
|
18708 | 135 |
val _ = Context.add_setup Induct.init; |
21506 | 136 |
val print_rules = Induct.print o Context.Proof; |
137 |
val dest_rules = dest o Induct.get o Context.Proof; |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
138 |
|
18637 | 139 |
val get_local = Induct.get o Context.Proof; |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
140 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
141 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
142 |
(* access rules *) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
143 |
|
18637 | 144 |
val lookup_casesT = lookup_rule o #1 o #1 o get_local; |
145 |
val lookup_casesS = lookup_rule o #2 o #1 o get_local; |
|
146 |
val lookup_inductT = lookup_rule o #1 o #2 o get_local; |
|
147 |
val lookup_inductS = lookup_rule o #2 o #2 o get_local; |
|
148 |
val lookup_coinductT = lookup_rule o #1 o #3 o get_local; |
|
149 |
val lookup_coinductS = lookup_rule o #2 o #3 o get_local; |
|
11730 | 150 |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
151 |
|
11730 | 152 |
fun find_rules which how ctxt x = |
18637 | 153 |
map snd (NetRules.retrieve (which (get_local ctxt)) (how x)); |
11730 | 154 |
|
155 |
val find_casesT = find_rules (#1 o #1) encode_type; |
|
18226 | 156 |
val find_casesS = find_rules (#2 o #1) I; |
11730 | 157 |
val find_inductT = find_rules (#1 o #2) encode_type; |
18226 | 158 |
val find_inductS = find_rules (#2 o #2) I; |
18210 | 159 |
val find_coinductT = find_rules (#1 o #3) encode_type; |
18226 | 160 |
val find_coinductS = find_rules (#2 o #3) I; |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
161 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
162 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
163 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
164 |
(** attributes **) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
165 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
166 |
local |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
167 |
|
18637 | 168 |
fun mk_att f g name arg = |
169 |
let val (x, thm) = g arg in (Induct.map (f (name, thm)) x, thm) end; |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
170 |
|
18210 | 171 |
fun map1 f (x, y, z) = (f x, y, z); |
172 |
fun map2 f (x, y, z) = (x, f y, z); |
|
173 |
fun map3 f (x, y, z) = (x, y, f z); |
|
174 |
||
175 |
fun add_casesT rule x = map1 (apfst (NetRules.insert rule)) x; |
|
176 |
fun add_casesS rule x = map1 (apsnd (NetRules.insert rule)) x; |
|
177 |
fun add_inductT rule x = map2 (apfst (NetRules.insert rule)) x; |
|
178 |
fun add_inductS rule x = map2 (apsnd (NetRules.insert rule)) x; |
|
179 |
fun add_coinductT rule x = map3 (apfst (NetRules.insert rule)) x; |
|
180 |
fun add_coinductS rule x = map3 (apsnd (NetRules.insert rule)) x; |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
181 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
182 |
fun consumes0 x = RuleCases.consumes_default 0 x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
183 |
fun consumes1 x = RuleCases.consumes_default 1 x; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
184 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
185 |
in |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
186 |
|
18637 | 187 |
val cases_type = mk_att add_casesT consumes0; |
188 |
val cases_set = mk_att add_casesS consumes1; |
|
189 |
val induct_type = mk_att add_inductT consumes0; |
|
190 |
val induct_set = mk_att add_inductS consumes1; |
|
191 |
val coinduct_type = mk_att add_coinductT consumes0; |
|
192 |
val coinduct_set = mk_att add_coinductS consumes1; |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
193 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
194 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
195 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
196 |
|
18637 | 197 |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
198 |
(** concrete syntax **) |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
199 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
200 |
val casesN = "cases"; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
201 |
val inductN = "induct"; |
18210 | 202 |
val coinductN = "coinduct"; |
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
203 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
204 |
val typeN = "type"; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
205 |
val setN = "set"; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
206 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
207 |
local |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
208 |
|
15703 | 209 |
fun spec k arg = |
210 |
Scan.lift (Args.$$$ k -- Args.colon) |-- arg || |
|
211 |
Scan.lift (Args.$$$ k) >> K ""; |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
212 |
|
18637 | 213 |
fun attrib add_type add_set = |
214 |
Attrib.syntax (spec typeN Args.tyname >> add_type || spec setN Args.const >> add_set); |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
215 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
216 |
in |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
217 |
|
18637 | 218 |
val cases_att = attrib cases_type cases_set; |
219 |
val induct_att = attrib induct_type induct_set; |
|
220 |
val coinduct_att = attrib coinduct_type coinduct_set; |
|
18210 | 221 |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
222 |
end; |
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
223 |
|
15801 | 224 |
val _ = Context.add_setup |
18708 | 225 |
(Attrib.add_attributes |
18728 | 226 |
[(casesN, cases_att, "declaration of cases rule for type or set"), |
227 |
(inductN, induct_att, "declaration of induction rule for type or set"), |
|
228 |
(coinductN, coinduct_att, "declaration of coinduction rule for type or set")]); |
|
11656
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
229 |
|
e499dceca569
moved HOL/Tools/induct_attrib.ML to Pure/Isar/induct_attrib.ML;
wenzelm
parents:
diff
changeset
|
230 |
end; |