summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/tactic.ML

changeset 19743 | 0843210d3756 |

parent 19532 | dae447f2b0b4 |

child 19925 | 3f9341831812 |

equal
deleted
inserted
replaced

19742:86f21beabafc | 19743:0843210d3756 |
---|---|

131 | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |
131 | seqcell => (tracing ("Subgoal " ^ string_of_int i ^ " selected"); |

132 Seq.make(fn()=> seqcell)); |
132 Seq.make(fn()=> seqcell)); |

133 |
133 |

134 (*Makes a rule by applying a tactic to an existing rule*) |
134 (*Makes a rule by applying a tactic to an existing rule*) |

135 fun rule_by_tactic tac rl = |
135 fun rule_by_tactic tac rl = |

136 let val (st, thaw) = freeze_thaw (zero_var_indexes rl) |
136 let val (st, thaw) = freeze_thaw_robust (zero_var_indexes rl) |

137 in case Seq.pull (tac st) of |
137 in case Seq.pull (tac st) of |

138 NONE => raise THM("rule_by_tactic", 0, [rl]) |
138 NONE => raise THM("rule_by_tactic", 0, [rl]) |

139 | SOME(st',_) => Thm.varifyT (thaw st') |
139 | SOME(st',_) => Thm.varifyT (thaw 0 st') |

140 end; |
140 end; |

141 |
141 |

142 (*** Basic tactics ***) |
142 (*** Basic tactics ***) |

143 |
143 |

144 (*** The following fail if the goal number is out of range: |
144 (*** The following fail if the goal number is out of range: |