src/bool/boolScript.sml

331 fun mk_eq(lhs,rhs)        = ���^lhs = ^rhs���;
421   let val e = mk_eq(y,t) in
448 val op== = mk_eq
520    SUBST theta1 (mk_eq(tm,subst theta0 template)) (REFL tm)
1163       val f_eq_g = mk_eq(f,g)
1164       val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
1415       val th2 = EXISTS (mk_exists(y,mk_eq(x,y)),x) th1
1416       val th3 = SPEC y (SPEC (mk_abs(y,mk_eq(x,y))) SELECT_AX)
2586        val template = mk_eq(t1l, mk_comb(rep,v))
2709       val MeqN = mk_eq(M,N)
2710       val x_eq_N = mk_eq(x,N)
2711       val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
2738      val x_eq_x' = mk_eq(x,x')
2739      val ctm = mk_imp(x', mk_eq(y,y'))
2770      val ctm1 = mk_imp(Q,  mk_eq(P,P'))
2771      val ctm2 = mk_imp(P', mk_eq(Q,Q'))
2802      val ctm1 = mk_eq(P,P')
2803      val ctm2 = mk_imp(P', mk_eq(Q,Q'))
2837      val PeqP'= mk_eq(P,P')
2838      val QeqQ'= mk_eq(Q,Q')
2888      val PeqP' = mk_eq(P,P')
2889      val ctm = mk_imp(notP',mk_eq(Q,Q'))
2903      val th14 = SUBS[SPECL [PeqP',ctm,mk_eq(PorQ,P'orQ')] AND_IMP_INTRO] th13
2925      val PeqQ = mk_eq(P,Q)
2926      val ctm1 = mk_imp(Q, mk_eq(x,x'))
2927      val ctm2 = mk_imp(mk_neg Q, mk_eq(y,y'))
2928      val target = mk_eq(mk_cond{cond=P,larm=x,rarm=y},
2976   val PeqQ_t = mk_eq(P, Q)
2988   val feqg_t = mk_forall(x, mk_imp(xINQ_t, mk_eq(mk_comb(f,x), mk_comb(g, x))))
3585     val xeqy = mk_eq(x,y)
3696       fun mk_eq th =
3699       (save_thm("RES_FORALL_THM", mk_eq RES_FORALL_DEF),
3700        save_thm("RES_EXISTS_THM", mk_eq RES_EXISTS_DEF),
3701        save_thm("RES_EXISTS_UNIQUE_THM", mk_eq RES_EXISTS_UNIQUE_DEF),
3702        save_thm("RES_SELECT_THM", mk_eq RES_SELECT_DEF))
3753      val fT_eq_T = mk_eq(fT,T)
3754      val fF_eq_T = mk_eq(fF,T)
3755      val fT_eq_F = mk_eq(fT,F)
3756      val fF_eq_F = mk_eq(fF,F)
3836      val f_eq_g = mk_eq(f,g)
3923       val MeqN = mk_eq(M,N)
3924       val x_eq_N = mk_eq(x,N)
3925       val fx_eq_gx = mk_eq(mk_comb(f,x),mk_comb(g,x))
3951     val eq = mk_eq(x,a)