Ticket #322: SC.thy
| File SC.thy, 407 bytes (added by , 14 years ago) |
|---|
| Line | |
|---|---|
| 1 | theory SC imports Main |
| 2 | begin |
| 3 | |
| 4 | ML {* |
| 5 | fun moo_tac ctxt (ct,i) = |
| 6 | let |
| 7 | val _ = (); |
| 8 | in |
| 9 | tracing ("Target: MOO!"); |
| 10 | no_tac |
| 11 | end; |
| 12 | *} |
| 13 | |
| 14 | method_setup moo = {* |
| 15 | Scan.succeed (fn ctxt => |
| 16 | SIMPLE_METHOD' (CSUBGOAL (moo_tac ctxt))) |
| 17 | *} "Some proof method reduced to a simple thing which fails." |
| 18 | |
| 19 | (* don't match on different state vars *) |
| 20 | lemma "X \<Longrightarrow> Y" |
| 21 | apply (moo) |
| 22 | |
| 23 | |
| 24 | end |
