changeset 42358 | b47d41d9f4b5 |
parent 38798 | 89f273ab1d42 |
child 42669 | 04dfffda5671 |
--- a/doc-src/TutorialI/Misc/Itrev.thy Sat Apr 16 12:46:18 2011 +0200 +++ b/doc-src/TutorialI/Misc/Itrev.thy Sat Apr 16 13:48:45 2011 +0200 @@ -2,7 +2,7 @@ theory Itrev imports Main begin -ML"unique_names := false" +declare [[unique_names = false]] (*>*) section{*Induction Heuristics*} @@ -141,6 +141,6 @@ \index{induction heuristics|)} *} (*<*) -ML"unique_names := true" +declare [[unique_names = true]] end (*>*)