| changeset 22902 | ac833b4bb7ee |
| parent 21687 | f689f729afab |
| child 23237 | ac9d126456e1 |
| 22901:481cd919c47f | 22902:ac833b4bb7ee |
|---|---|
47 (* |
47 (* |
48 -------- (init) |
48 -------- (init) |
49 C ==> #C |
49 C ==> #C |
50 *) |
50 *) |
51 val init = |
51 val init = |
52 let val A = #1 (Drule.dest_implies (Thm.cprop_of Drule.protectI)) |
52 let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI)) |
53 in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end; |
53 in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end; |
54 |
54 |
55 (* |
55 (* |
56 C |
56 C |
57 --- (protect) |
57 --- (protect) |