equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Itrev |
2 theory Itrev |
3 imports Main |
3 imports Main |
4 begin |
4 begin |
5 ML"Unsynchronized.reset NameSpace.unique_names" |
5 ML"Unsynchronized.reset unique_names" |
6 (*>*) |
6 (*>*) |
7 |
7 |
8 section{*Induction Heuristics*} |
8 section{*Induction Heuristics*} |
9 |
9 |
10 text{*\label{sec:InductionHeuristics} |
10 text{*\label{sec:InductionHeuristics} |
139 Additionally, you can read \S\ref{sec:advanced-ind} |
139 Additionally, you can read \S\ref{sec:advanced-ind} |
140 to learn about some advanced techniques for inductive proofs.% |
140 to learn about some advanced techniques for inductive proofs.% |
141 \index{induction heuristics|)} |
141 \index{induction heuristics|)} |
142 *} |
142 *} |
143 (*<*) |
143 (*<*) |
144 ML"Unsynchronized.set NameSpace.unique_names" |
144 ML"Unsynchronized.set unique_names" |
145 end |
145 end |
146 (*>*) |
146 (*>*) |