# HG changeset patch
# User haftmann
# Date 1285333898 -7200
# Node ID 066e2d4d0de89757faf2ef0b1401b8fcd9eb6b86
# Parent  a0d49ed5a23a3ad5f550b6cd67723d34d23a2402
avoid fragile tranclp syntax; corrected resolution; corrected typo

diff -r a0d49ed5a23a -r 066e2d4d0de8 doc-src/Codegen/Thy/Inductive_Predicate.thy
--- a/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Sep 24 14:56:16 2010 +0200
+++ b/doc-src/Codegen/Thy/Inductive_Predicate.thy	Fri Sep 24 15:11:38 2010 +0200
@@ -113,8 +113,8 @@
 *}
 
 text %quote {*
-  @{thm tranclp.intros(1)[of r a b]} \\
-  @{thm tranclp.intros(2)[of r a b c]}
+  @{lemma [source] "r a b \<Longrightarrow> tranclp r a b" by (fact tranclp.intros(1))}\\
+  @{lemma [source] "tranclp r a b \<Longrightarrow> r b c \<Longrightarrow> tranclp r a c" by (fact tranclp.intros(2))}
 *}
 
 text {*
@@ -127,8 +127,8 @@
 *}
 
 lemma %quote [code_pred_intro]:
-  "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ a b"
-  "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c"
+  "r a b \<Longrightarrow> tranclp r a b"
+  "r a b \<Longrightarrow> tranclp r b c \<Longrightarrow> tranclp r a c"
 by auto
 
 text {*
@@ -142,7 +142,7 @@
 code_pred %quote tranclp
 proof -
   case tranclp
-  from this converse_tranclpE [OF this(1)] show thesis by metis
+  from this converse_tranclpE [OF tranclp.prems] show thesis by metis
 qed
 
 text {*
@@ -152,7 +152,7 @@
 *}
 
 text %quote {*
-  @{thm [display] lexord_def[of "r"]}
+  @{thm [display] lexord_def [of r]}
 *}
 
 text {*
@@ -260,7 +260,7 @@
 
 text {*
   Further examples for compiling inductive predicates can be found in
-  the @{text "HOL/ex/Predicate_Compile_ex,thy"} theory file.  There are
+  the @{text "HOL/ex/Predicate_Compile_ex.thy"} theory file.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   @{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
   sessions.
diff -r a0d49ed5a23a -r 066e2d4d0de8 doc-src/Codegen/Thy/document/Inductive_Predicate.tex
--- a/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Fri Sep 24 14:56:16 2010 +0200
+++ b/doc-src/Codegen/Thy/document/Inductive_Predicate.tex	Fri Sep 24 15:11:38 2010 +0200
@@ -245,8 +245,8 @@
 \isatagquote
 %
 \begin{isamarkuptext}%
-\isa{r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b} \\
-  \isa{r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c}%
+\isa{{\isachardoublequote}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ a\ b{\isachardoublequote}}\\
+  \isa{{\isachardoublequote}tranclp\ r\ a\ b\ {\isasymLongrightarrow}\ r\ b\ c\ {\isasymLongrightarrow}\ tranclp\ r\ a\ c{\isachardoublequote}}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -273,8 +273,8 @@
 \isatagquote
 \isacommand{lemma}\isamarkupfalse%
 \ {\isacharbrackleft}code{\isacharunderscore}pred{\isacharunderscore}intro{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ b{\isachardoublequoteclose}\isanewline
-\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ b\ c\ {\isasymLongrightarrow}\ r\isactrlsup {\isacharplus}\isactrlsup {\isacharplus}\ a\ c{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ a\ b{\isachardoublequoteclose}\isanewline
+\ \ {\isachardoublequoteopen}r\ a\ b\ {\isasymLongrightarrow}\ tranclp\ r\ b\ c\ {\isasymLongrightarrow}\ tranclp\ r\ a\ c{\isachardoublequoteclose}\isanewline
 \isacommand{by}\isamarkupfalse%
 \ auto%
 \endisatagquote
@@ -305,7 +305,7 @@
 \ \ \isacommand{case}\isamarkupfalse%
 \ tranclp\isanewline
 \ \ \isacommand{from}\isamarkupfalse%
-\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ this{\isacharparenleft}{\isadigit{1}}{\isacharparenright}{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
+\ this\ converse{\isacharunderscore}tranclpE\ {\isacharbrackleft}OF\ tranclp{\isachardot}prems{\isacharbrackright}\ \isacommand{show}\isamarkupfalse%
 \ thesis\ \isacommand{by}\isamarkupfalse%
 \ metis\isanewline
 \isacommand{qed}\isamarkupfalse%
@@ -471,7 +471,7 @@
 %
 \begin{isamarkuptext}%
 Further examples for compiling inductive predicates can be found in
-  the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isacharcomma}thy} theory file.  There are
+  the \isa{HOL{\isacharslash}ex{\isacharslash}Predicate{\isacharunderscore}Compile{\isacharunderscore}ex{\isachardot}thy} theory file.  There are
   also some examples in the Archive of Formal Proofs, notably in the
   \isa{POPLmark{\isacharminus}deBruijn} and the \isa{FeatherweightJava}
   sessions.%