Mercurial Mercurial > hg > isabelle-cookbook / 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.
ProgTutorial/Package/Ind_Extensions.thy
changeset 551 be361e980acf
parent 546 d84867127c5d
child 560 8d30446d89f0 
--- a/ProgTutorial/Package/Ind_Extensions.thy	Wed Jul 31 15:44:28 2013 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Sat Aug 31 08:07:45 2013 +0100
@@ -135,7 +135,7 @@
   form
 
   \begin{isabelle}
-  @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^isup>* \<Longrightarrow> pred ts"}
+  @{text "rule ::= \<And>xs. As \<Longrightarrow> (\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>* \<Longrightarrow> pred ts"}
   \end{isabelle}
 
   where the @{text "As"} and @{text "Bs"} can be any collection of formulae
isabelle-cookbook