# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1279896120 -7200
# Node ID 41899210aafb665cdc300c2dcb28a79a06c1b464
# Parent  76434267652057d6a5ec91e830df62dacf9330a7
made compatible

diff -r 764342676520 -r 41899210aafb Pearl/Paper.thy
--- a/Pearl/Paper.thy	Fri Jul 23 16:41:36 2010 +0200
+++ b/Pearl/Paper.thy	Fri Jul 23 16:42:00 2010 +0200
@@ -347,7 +347,7 @@
   @{thm zero_perm_def[no_vars, THEN eq_reflection]} \hspace{4mm}
   @{thm plus_perm_def[where p="\<pi>\<^isub>1" and q="\<pi>\<^isub>2", THEN eq_reflection]} \hspace{4mm}
   @{thm uminus_perm_def[where p="\<pi>", THEN eq_reflection]} \hspace{4mm}
-  @{thm diff_def[where x="\<pi>\<^isub>1" and y="\<pi>\<^isub>2"]} 
+  @{thm diff_def[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2"]} 
   \end{tabular}
   \end{isabelle}