src/FOLP/simpdata.ML
changeset 2603 4988dda71c0b
parent 1463 49ca5e875691
child 3836 f1a1817659e6
equal deleted inserted replaced
2602:5ac837d98a85 2603:4988dda71c0b
     8 
     8 
     9 (*** Rewrite rules ***)
     9 (*** Rewrite rules ***)
    10 
    10 
    11 fun int_prove_fun_raw s = 
    11 fun int_prove_fun_raw s = 
    12     (writeln s;  prove_goal IFOLP.thy s
    12     (writeln s;  prove_goal IFOLP.thy s
    13        (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
    13        (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
    14 
    14 
    15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
    15 fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
    16 
    16 
    17 val conj_rews = map int_prove_fun
    17 val conj_rews = map int_prove_fun
    18  ["P & True <-> P",     "True & P <-> P",
    18  ["P & True <-> P",     "True & P <-> P",