# HG changeset patch
# User traytel
# Date 1350049975 -7200
# Node ID 9cbec40e88eab064f22c58ce06887a288993b1cb
# Parent  4cbb7b19b03b71aae47ed6d15950ded1e7554f71
disambiguated grammar

diff -r 4cbb7b19b03b -r 9cbec40e88ea src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy
--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy	Fri Oct 12 15:52:45 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Parallel.thy	Fri Oct 12 15:52:55 2012 +0200
@@ -11,15 +11,15 @@
 imports Tree
 begin
 
-
+no_notation plus_class.plus (infixl "+" 65)
+no_notation Sublist.parallel (infixl "\<parallel>" 50)
+    
 consts Nplus :: "N \<Rightarrow> N \<Rightarrow> N" (infixl "+" 60)
 
 axiomatization where
     Nplus_comm: "(a::N) + b = b + (a::N)"
 and Nplus_assoc: "((a::N) + b) + c = a + (b + c)"
 
-
-
 section{* Parallel composition *}
 
 fun par_r where "par_r (tr1,tr2) = root tr1 + root tr2"