equal
deleted
inserted
replaced
35 |
35 |
36 ML {* iff_oracle (the_context ()) 2 *} |
36 ML {* iff_oracle (the_context ()) 2 *} |
37 ML {* iff_oracle (the_context ()) 10 *} |
37 ML {* iff_oracle (the_context ()) 10 *} |
38 ML {* #der (Thm.rep_thm it) *} |
38 ML {* #der (Thm.rep_thm it) *} |
39 |
39 |
40 text {* These oracle calls had better fail *} |
40 text {* These oracle calls had better fail. *} |
41 |
41 |
42 ML {* |
42 ML {* |
43 (iff_oracle (the_context ()) 5; error "?") |
43 (iff_oracle (the_context ()) 5; error "?") |
44 handle Fail _ => warning "Oracle failed, as expected" |
44 handle Fail _ => tracing "Oracle failed, as expected" |
45 *} |
45 *} |
46 |
46 |
47 ML {* |
47 ML {* |
48 (iff_oracle (the_context ()) 1; error "?") |
48 (iff_oracle (the_context ()) 1; error "?") |
49 handle Fail _ => warning "Oracle failed, as expected" |
49 handle Fail _ => tracing "Oracle failed, as expected" |
50 *} |
50 *} |
51 |
51 |
52 |
52 |
53 subsection {* Oracle as proof method *} |
53 subsection {* Oracle as proof method *} |
54 |
54 |