corrected for the translation from _ to __ in c_COMBx_e
authorpaulson
Thu Sep 21 17:31:10 2006 +0200 (2006-09-21)
changeset 206608606ddd42554
parent 20659 66b8455090b8
child 20661 46832fee1215
corrected for the translation from _ to __ in c_COMBx_e
src/HOL/Tools/atp-inputs/const_combBC_e.dfg
src/HOL/Tools/atp-inputs/const_combBC_e.tptp
src/HOL/Tools/atp-inputs/const_combS_e.dfg
src/HOL/Tools/atp-inputs/const_combS_e.tptp
src/HOL/Tools/atp-inputs/full_combBC_e.dfg
src/HOL/Tools/atp-inputs/full_combBC_e.tptp
src/HOL/Tools/atp-inputs/full_combS_e.dfg
src/HOL/Tools/atp-inputs/full_combS_e.tptp
src/HOL/Tools/atp-inputs/par_combBC_e.dfg
src/HOL/Tools/atp-inputs/par_combBC_e.tptp
src/HOL/Tools/atp-inputs/par_combS_e.dfg
src/HOL/Tools/atp-inputs/par_combS_e.tptp
src/HOL/Tools/atp-inputs/u_combBC_e.dfg
src/HOL/Tools/atp-inputs/u_combBC_e.tptp
src/HOL/Tools/atp-inputs/u_combS_e.dfg
src/HOL/Tools/atp-inputs/u_combS_e.tptp
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/atp-inputs/const_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
     1.2 +++ b/src/HOL/Tools/atp-inputs/const_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
     1.3 @@ -4,10 +4,10 @@
     1.4  
     1.5  clause(
     1.6  forall([A, B, C, F, G, U, V, X],
     1.7 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
     1.8 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
     1.9  a6 ).
    1.10  
    1.11  clause(
    1.12  forall([A, B, C, F, G, U, V, X],
    1.13 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
    1.14 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
    1.15  a7 ).
     2.1 --- a/src/HOL/Tools/atp-inputs/const_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
     2.2 +++ b/src/HOL/Tools/atp-inputs/const_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
     2.3 @@ -4,10 +4,10 @@
     2.4  
     2.5  %B' c f g x -->  c (f (g x))
     2.6  input_clause(a6,axiom,
     2.7 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
     2.8 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e(A,B,U,V),C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
     2.9  
    2.10  %C' c f g x --> c (f x) g
    2.11  input_clause(a7,axiom,
    2.12 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
    2.13 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
    2.14  
    2.15  
     3.1 --- a/src/HOL/Tools/atp-inputs/const_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
     3.2 +++ b/src/HOL/Tools/atp-inputs/const_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
     3.3 @@ -4,5 +4,5 @@
     3.4  
     3.5  clause(
     3.6  forall([A, B, C, F, G, U, V, X],
     3.7 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
     3.8 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
     3.9  a8 ).
     4.1 --- a/src/HOL/Tools/atp-inputs/const_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
     4.2 +++ b/src/HOL/Tools/atp-inputs/const_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
     4.3 @@ -4,4 +4,4 @@
     4.4  
     4.5  %S' c f g x --> c (f x) (g x)
     4.6  input_clause(a8,axiom,
     4.7 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
     4.8 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e(A,B,U,V),C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
     5.1 --- a/src/HOL/Tools/atp-inputs/full_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
     5.2 +++ b/src/HOL/Tools/atp-inputs/full_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
     5.3 @@ -4,10 +4,10 @@
     5.4  
     5.5  clause(
     5.6  forall([A, B, C, F, G, U, V, X],
     5.7 -or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB_e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B)))),
     5.8 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB__e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B)))),
     5.9  a6 ).
    5.10  
    5.11  clause(
    5.12  forall([A, B, C, F, G, U, V, X],
    5.13 -or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U)))),
    5.14 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U)))),
    5.15  a7 ).
     6.1 --- a/src/HOL/Tools/atp-inputs/full_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
     6.2 +++ b/src/HOL/Tools/atp-inputs/full_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
     6.3 @@ -4,9 +4,9 @@
     6.4  
     6.5  %B' c f g x -->  c (f (g x))
     6.6  input_clause(a6,axiom,
     6.7 -[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB_e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B))]).
     6.8 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBB__e,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),typeinfo(C,tc_fun(A,B))),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),typeinfo(F,tc_fun(U,A))),tc_fun(tc_fun(V,U),tc_fun(V,B))),typeinfo(G,tc_fun(V,U))),tc_fun(V,B)),typeinfo(X,V)),B),typeinfo(hAPP(typeinfo(C,tc_fun(A,B)),typeinfo(hAPP(typeinfo(F,tc_fun(U,A)),typeinfo(hAPP(typeinfo(G,tc_fun(V,U)),typeinfo(X,V)),U)),A)),B))]).
     6.9  
    6.10  
    6.11  %C' c f g x --> c (f x) g
    6.12  input_clause(a7,axiom,
    6.13 -[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U))]).
    6.14 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBC__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(B,tc_fun(V,U))),typeinfo(G,B)),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(G,B)),U))]).
     7.1 --- a/src/HOL/Tools/atp-inputs/full_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
     7.2 +++ b/src/HOL/Tools/atp-inputs/full_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
     7.3 @@ -4,6 +4,6 @@
     7.4  
     7.5  clause(
     7.6  forall([A, B, C, F, G, U, V, X],
     7.7 -or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U)))),
     7.8 +or( equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U)))),
     7.9  a8 ).
    7.10  
     8.1 --- a/src/HOL/Tools/atp-inputs/full_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
     8.2 +++ b/src/HOL/Tools/atp-inputs/full_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
     8.3 @@ -5,4 +5,4 @@
     8.4  
     8.5  %S' c f g x --> c (f x) (g x)
     8.6  input_clause(a8,axiom,
     8.7 -[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS_e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U))]).
     8.8 +[++equal(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(hAPP(typeinfo(c_COMBS__e,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),typeinfo(C,tc_fun(A,tc_fun(B,U)))),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),typeinfo(F,tc_fun(V,A))),tc_fun(tc_fun(V,B),tc_fun(V,U))),typeinfo(G,tc_fun(V,B))),tc_fun(V,U)),typeinfo(X,V)),U),typeinfo(hAPP(typeinfo(hAPP(typeinfo(C,tc_fun(A,tc_fun(B,U))),typeinfo(hAPP(typeinfo(F,tc_fun(V,A)),typeinfo(X,V)),A)),tc_fun(B,U)),typeinfo(hAPP(typeinfo(G,tc_fun(V,B)),typeinfo(X,V)),B)),U))]).
     9.1 --- a/src/HOL/Tools/atp-inputs/par_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
     9.2 +++ b/src/HOL/Tools/atp-inputs/par_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
     9.3 @@ -4,10 +4,10 @@
     9.4  
     9.5  clause(
     9.6  forall([A, B, C, F, G, U, V, X],
     9.7 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B))))),
     9.8 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B))))),
     9.9  a6 ).
    9.10  
    9.11  clause(
    9.12  forall([A, B, C, F, G, U, V, X],
    9.13 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U))))),
    9.14 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U))))),
    9.15  a7 ).
    10.1 --- a/src/HOL/Tools/atp-inputs/par_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
    10.2 +++ b/src/HOL/Tools/atp-inputs/par_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
    10.3 @@ -4,8 +4,8 @@
    10.4  
    10.5  %B' c f g x -->  c (f (g x))
    10.6  input_clause(a6,axiom,
    10.7 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B)))]).
    10.8 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C,tc_fun(tc_fun(A,B),tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B))))),F,tc_fun(tc_fun(U,A),tc_fun(tc_fun(V,U),tc_fun(V,B)))),G,tc_fun(tc_fun(V,U),tc_fun(V,B))),X,tc_fun(V,B)),hAPP(C,hAPP(F,hAPP(G,X,tc_fun(V,U)),tc_fun(U,A)),tc_fun(A,B)))]).
    10.9  
   10.10  %C' c f g x --> c (f x) g
   10.11  input_clause(a7,axiom,
   10.12 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U)))]).
   10.13 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(B,tc_fun(V,U)))),G,tc_fun(B,tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),G,tc_fun(B,U)))]).
    11.1 --- a/src/HOL/Tools/atp-inputs/par_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
    11.2 +++ b/src/HOL/Tools/atp-inputs/par_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
    11.3 @@ -4,5 +4,5 @@
    11.4  
    11.5  clause(
    11.6  forall([A, B, C, F, G, U, V, X],
    11.7 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U))))),
    11.8 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U))))),
    11.9  a8 ).
    12.1 --- a/src/HOL/Tools/atp-inputs/par_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
    12.2 +++ b/src/HOL/Tools/atp-inputs/par_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
    12.3 @@ -4,5 +4,5 @@
    12.4  
    12.5  %S' c f g x --> c (f x) (g x)
    12.6  input_clause(a8,axiom,
    12.7 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U)))]).
    12.8 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C,tc_fun(tc_fun(A,tc_fun(B,U)),tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U))))),F,tc_fun(tc_fun(V,A),tc_fun(tc_fun(V,B),tc_fun(V,U)))),G,tc_fun(tc_fun(V,B),tc_fun(V,U))),X,tc_fun(V,U)),hAPP(hAPP(C,hAPP(F,X,tc_fun(V,A)),tc_fun(A,tc_fun(B,U))),hAPP(G,X,tc_fun(V,B)),tc_fun(B,U)))]).
    12.9  
    13.1 --- a/src/HOL/Tools/atp-inputs/u_combBC_e.dfg	Thu Sep 21 16:45:53 2006 +0200
    13.2 +++ b/src/HOL/Tools/atp-inputs/u_combBC_e.dfg	Thu Sep 21 17:31:10 2006 +0200
    13.3 @@ -4,10 +4,10 @@
    13.4  
    13.5  clause(
    13.6  forall([C, F, G, X],
    13.7 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
    13.8 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X)))))),
    13.9  a6 ).
   13.10  
   13.11  clause(
   13.12  forall([C, F, G, X],
   13.13 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
   13.14 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G)))),
   13.15  a7 ).
    14.1 --- a/src/HOL/Tools/atp-inputs/u_combBC_e.tptp	Thu Sep 21 16:45:53 2006 +0200
    14.2 +++ b/src/HOL/Tools/atp-inputs/u_combBC_e.tptp	Thu Sep 21 17:31:10 2006 +0200
    14.3 @@ -4,8 +4,8 @@
    14.4  
    14.5  %B' c f g x -->  c (f (g x))
    14.6  input_clause(a6,axiom,
    14.7 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB_e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
    14.8 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBB__e,C),F),G),X),hAPP(C,hAPP(F,hAPP(G,X))))]).
    14.9  
   14.10  %C' c f g x --> c (f x) g
   14.11  input_clause(a7,axiom,
   14.12 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
   14.13 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBC__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),G))]).
    15.1 --- a/src/HOL/Tools/atp-inputs/u_combS_e.dfg	Thu Sep 21 16:45:53 2006 +0200
    15.2 +++ b/src/HOL/Tools/atp-inputs/u_combS_e.dfg	Thu Sep 21 17:31:10 2006 +0200
    15.3 @@ -4,5 +4,5 @@
    15.4  
    15.5  clause(
    15.6  forall([C, F, G, X],
    15.7 -or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
    15.8 +or( equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X))))),
    15.9  a8 ).
    16.1 --- a/src/HOL/Tools/atp-inputs/u_combS_e.tptp	Thu Sep 21 16:45:53 2006 +0200
    16.2 +++ b/src/HOL/Tools/atp-inputs/u_combS_e.tptp	Thu Sep 21 17:31:10 2006 +0200
    16.3 @@ -4,4 +4,4 @@
    16.4  
    16.5  %S' c f g x --> c (f x) (g x)
    16.6  input_clause(a8,axiom,
    16.7 -[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS_e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
    16.8 +[++equal(hAPP(hAPP(hAPP(hAPP(c_COMBS__e,C),F),G),X),hAPP(hAPP(C,hAPP(F,X)),hAPP(G,X)))]).
    17.1 --- a/src/HOL/Tools/res_hol_clause.ML	Thu Sep 21 16:45:53 2006 +0200
    17.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Thu Sep 21 17:31:10 2006 +0200
    17.3 @@ -794,7 +794,8 @@
    17.4  
    17.5  fun init_funcs_tab funcs = 
    17.6      let val tp = !typ_level
    17.7 -	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC","c_COMBB_e","c_COMBC_e","c_COMBS_e"]
    17.8 +	val funcs0 = foldl init_combs funcs ["c_COMBK","c_COMBS","c_COMBI","c_COMBB","c_COMBC",
    17.9 +	                                     "c_COMBB__e","c_COMBC__e","c_COMBS__e"]
   17.10  	val funcs1 = case tp of T_PARTIAL => Symtab.update ("hAPP",3) funcs0
   17.11  				      | _ => Symtab.update ("hAPP",2) funcs0
   17.12  	val funcs2 = case tp of T_FULL => Symtab.update ("typeinfo",2) funcs1