equal
deleted
inserted
replaced
33 |
33 |
34 subsection {* Oracle as low-level rule *} |
34 subsection {* Oracle as low-level rule *} |
35 |
35 |
36 ML {* iff_oracle @{theory} 2 *} |
36 ML {* iff_oracle @{theory} 2 *} |
37 ML {* iff_oracle @{theory} 10 *} |
37 ML {* iff_oracle @{theory} 10 *} |
38 ML {* #der (Thm.rep_thm it) *} |
|
39 |
38 |
40 text {* These oracle calls had better fail. *} |
39 text {* These oracle calls had better fail. *} |
41 |
40 |
42 ML {* |
41 ML {* |
43 (iff_oracle @{theory} 5; error "?") |
42 (iff_oracle @{theory} 5; error "?") |