Lines Matching defs:con
184 `!con : 'a->'b.
189 (!k. hom(CON k) = con k) /\
194 THEN Q.EXISTS_TAC `\x. HOM (con:'a ->'b) var lam app (REP_nc x)`
200 `!con : 'a->'b.
205 (!k. hom(CON k) = con k) /\
354 val con = Term`\k:'a. (CON k, (con k:'b) )`
361 val th1 = SPECL [con,var,app,lam] instth
377 ((!k. SND p(CON k) = con k) /\
391 val con = Term`\k. CON k:'a nc` and
395 val th1 = BETA_RULE (SPECL [con,var,app,lam] instth)
419 (!k. SND p (CON k) = con k) /\
425 (!k. SND p(CON k) = con k) /\
451 val th3_0 = Q.INST [`var` |-> `var`, `con` |-> `con`,
462 `!con:'a -> 'b.
467 (!k. hom(CON k) = con k) /\
476 `!con var app lam.
478 (!k. hom (CON k) = con k) /\
484 Q.SPECL [`con`, `var`, `\ht hu t u. app t u ht hu`,
585 val con = Term`\x:'a. T` and
589 val th1 = BETA_RULE (SPECL [con,var,app,lam] instth)
1071 Q.INST [`con` |-> `\x. 1`, `var` |-> `\s. 1`,