src/FOL/simpdata.ML
changeset 13149 773657d466cb
parent 12825 f1f7964ed05c
child 13462 56610e2ba220
equal deleted inserted replaced
13148:fe118a977a6d 13149:773657d466cb
    55 bind_thms ("quant_simps", map int_prove_fun
    55 bind_thms ("quant_simps", map int_prove_fun
    56  ["(ALL x. P) <-> P",
    56  ["(ALL x. P) <-> P",
    57   "(ALL x. x=t --> P(x)) <-> P(t)",
    57   "(ALL x. x=t --> P(x)) <-> P(t)",
    58   "(ALL x. t=x --> P(x)) <-> P(t)",
    58   "(ALL x. t=x --> P(x)) <-> P(t)",
    59   "(EX x. P) <-> P",
    59   "(EX x. P) <-> P",
       
    60   "EX x. x=t", "EX x. t=x",
    60   "(EX x. x=t & P(x)) <-> P(t)",
    61   "(EX x. x=t & P(x)) <-> P(t)",
    61   "(EX x. t=x & P(x)) <-> P(t)"]);
    62   "(EX x. t=x & P(x)) <-> P(t)"]);
    62 
    63 
    63 (*These are NOT supplied by default!*)
    64 (*These are NOT supplied by default!*)
    64 bind_thms ("distrib_simps", map int_prove_fun
    65 bind_thms ("distrib_simps", map int_prove_fun