# HG changeset patch
# User paulson
# Date 991386259 -7200
# Node ID 29f8b00d7e1f0f5b3ebcdb67243fd1ac915eb379
# Parent  416ea5c009f54ff34b5453e42c970b0e719f4eb3
renamed # to ## to avoid clashing with List cons

diff -r 416ea5c009f5 -r 29f8b00d7e1f src/HOL/Induct/Comb.ML
--- a/src/HOL/Induct/Comb.ML	Fri Jun 01 11:03:50 2001 +0200
+++ b/src/HOL/Induct/Comb.ML	Fri Jun 01 11:04:19 2001 +0200
@@ -47,7 +47,7 @@
 (*Derive a case for each combinator constructor*)
 val K_contractE  = contract.mk_cases "K -1-> z";
 val S_contractE  = contract.mk_cases "S -1-> z";
-val Ap_contractE = contract.mk_cases "x#y -1-> z";
+val Ap_contractE = contract.mk_cases "x##y -1-> z";
 
 AddSIs [contract.K, contract.S];
 AddIs  [contract.Ap1, contract.Ap2];
@@ -58,32 +58,32 @@
 qed "I_contract_E";
 AddSEs [I_contract_E];
 
-Goal "K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
+Goal "K##x -1-> z ==> (EX x'. z = K##x' & x -1-> x')";
 by (Blast_tac 1);
 qed "K1_contractD";
 AddSEs [K1_contractD];
 
-Goal "x ---> y ==> x#z ---> y#z";
+Goal "x ---> y ==> x##z ---> y##z";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
 qed "Ap_reduce1";
 
-Goal "x ---> y ==> z#x ---> z#y";
+Goal "x ---> y ==> z##x ---> z##y";
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
 qed "Ap_reduce2";
 
 (** Counterexample to the diamond property for -1-> **)
 
-Goal "K#I#(I#I) -1-> I";
+Goal "K##I##(I##I) -1-> I";
 by (rtac contract.K 1);
 qed "KIII_contract1";
 
-Goalw [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
+Goalw [I_def] "K##I##(I##I) -1-> K##I##((K##I)##(K##I))";
 by (Blast_tac 1);
 qed "KIII_contract2";
 
-Goal "K#I#((K#I)#(K#I)) -1-> I";
+Goal "K##I##((K##I)##(K##I)) -1-> I";
 by (Blast_tac 1);
 qed "KIII_contract3";
 
@@ -98,7 +98,7 @@
 (*Derive a case for each combinator constructor*)
 val K_parcontractE  = parcontract.mk_cases "K =1=> z";
 val S_parcontractE  = parcontract.mk_cases "S =1=> z";
-val Ap_parcontractE = parcontract.mk_cases "x#y =1=> z";
+val Ap_parcontractE = parcontract.mk_cases "x##y =1=> z";
 
 AddSIs [parcontract.refl, parcontract.K, parcontract.S];
 AddIs  [parcontract.Ap];
@@ -106,17 +106,17 @@
 
 (*** Basic properties of parallel contraction ***)
 
-Goal "K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
+Goal "K##x =1=> z ==> (EX x'. z = K##x' & x =1=> x')";
 by (Blast_tac 1);
 qed "K1_parcontractD";
 AddSDs [K1_parcontractD];
 
-Goal "S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
+Goal "S##x =1=> z ==> (EX x'. z = S##x' & x =1=> x')";
 by (Blast_tac 1);
 qed "S1_parcontractD";
 AddSDs [S1_parcontractD];
 
-Goal "S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
+Goal "S##x##y =1=> z ==> (EX x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')";
 by (Blast_tac 1);
 qed "S2_parcontractD";
 AddSDs [S2_parcontractD];
@@ -148,7 +148,7 @@
 AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
 
 (*Example only: not used*)
-Goalw [I_def] "I#x ---> x";
+Goalw [I_def] "I##x ---> x";
 by (Blast_tac 1);
 qed "reduce_I";
 
diff -r 416ea5c009f5 -r 29f8b00d7e1f src/HOL/Induct/Comb.thy
--- 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"