equal
deleted
inserted
replaced
9 uses |
9 uses |
10 "~~/src/Provers/classical.ML" |
10 "~~/src/Provers/classical.ML" |
11 "~~/src/Provers/blast.ML" |
11 "~~/src/Provers/blast.ML" |
12 "~~/src/Provers/clasimp.ML" |
12 "~~/src/Provers/clasimp.ML" |
13 "~~/src/Tools/induct.ML" |
13 "~~/src/Tools/induct.ML" |
|
14 "~~/src/Tools/case_product.ML" |
14 ("cladata.ML") |
15 ("cladata.ML") |
15 ("simpdata.ML") |
16 ("simpdata.ML") |
16 begin |
17 begin |
17 |
18 |
18 |
19 |
389 *} |
390 *} |
390 |
391 |
391 setup Induct.setup |
392 setup Induct.setup |
392 declare case_split [cases type: o] |
393 declare case_split [cases type: o] |
393 |
394 |
|
395 setup Case_Product.setup |
|
396 |
394 |
397 |
395 hide_const (open) eq |
398 hide_const (open) eq |
396 |
399 |
397 end |
400 end |