Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/CTL/PDL.thy
changeset 21202 6649bf75b9dc
parent 18724 cb6e0064c88c
child 27015 f8537d69f514 
--- a/doc-src/TutorialI/CTL/PDL.thy	Tue Nov 07 09:59:43 2006 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Tue Nov 07 11:28:25 2006 +0100
@@ -102,7 +102,7 @@
 which is proved by @{term lfp}-induction:
 *}
 
- apply(erule lfp_induct)
+ apply(erule lfp_induct_set)
   apply(rule mono_ef)
  apply(simp)
 (*pr(latex xsymbols symbols);*)
isabelle