# HG changeset patch
# User wenzelm
# Date 1451502679 -3600
# Node ID df64653779e17788a9f2a0278134e1d56f1d6146
# Parent  39e4a93ad36e11751b0fe4108fb18f926512144b
removed junk;

diff -r 39e4a93ad36e -r df64653779e1 src/Doc/Tutorial/CTL/PDL.thy
--- a/src/Doc/Tutorial/CTL/PDL.thy	Wed Dec 30 20:07:59 2015 +0100
+++ b/src/Doc/Tutorial/CTL/PDL.thy	Wed Dec 30 20:11:19 2015 +0100
@@ -98,7 +98,6 @@
  apply(erule lfp_induct_set)
   apply(rule mono_ef)
  apply(simp)
-(*pr(latex xsymbols symbols);*)
 txt{*\noindent
 Having disposed of the monotonicity subgoal,
 simplification leaves us with the following goal: