src/HOL/Induct/Comb.thy
changeset 11359 29f8b00d7e1f
parent 9101 b643f4d7b9e9
child 13075 d3e1d554cd6d
--- a/src/HOL/Induct/Comb.thy	Fri Jun 01 11:03:50 2001 +0200
+++ b/src/HOL/Induct/Comb.thy	Fri Jun 01 11:04:19 2001 +0200
@@ -18,7 +18,7 @@
 (** Datatype definition of combinators S and K, with infixed application **)
 datatype comb = K
               | S
-              | "#" comb comb (infixl 90)
+              | "##" comb comb (infixl 90)
 
 (** Inductive definition of contractions, -1->
              and (multi-step) reductions, --->
@@ -34,10 +34,10 @@
 
 inductive contract
   intrs
-    K     "K#x#y -1-> x"
-    S     "S#x#y#z -1-> (x#z)#(y#z)"
-    Ap1   "x-1->y ==> x#z -1-> y#z"
-    Ap2   "x-1->y ==> z#x -1-> z#y"
+    K     "K##x##y -1-> x"
+    S     "S##x##y##z -1-> (x##z)##(y##z)"
+    Ap1   "x-1->y ==> x##z -1-> y##z"
+    Ap2   "x-1->y ==> z##x -1-> z##y"
 
 
 (** Inductive definition of parallel contractions, =1=>
@@ -55,15 +55,15 @@
 inductive parcontract
   intrs
     refl  "x =1=> x"
-    K     "K#x#y =1=> x"
-    S     "S#x#y#z =1=> (x#z)#(y#z)"
-    Ap    "[| x=1=>y;  z=1=>w |] ==> x#z =1=> y#w"
+    K     "K##x##y =1=> x"
+    S     "S##x##y##z =1=> (x##z)##(y##z)"
+    Ap    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"
 
 
 (*Misc definitions*)
 constdefs
   I :: comb
-  "I == S#K#K"
+  "I == S##K##K"
 
   (*confluence; Lambda/Commutation treats this more abstractly*)
   diamond   :: "('a * 'a)set => bool"