Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Adapted to changes in FixedPoint theory.
authorberghofe
Tue, 07 Nov 2006 11:28:25 +0100
changeset 21202 6649bf75b9dc
parent 21201 803bc7672d17
child 21203 8154a62bb498
Adapted to changes in FixedPoint theory.
doc-src/TutorialI/CTL/PDL.thy file | annotate | diff | comparison | revisions 
--- 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