src/FOL/ROOT.ML
changeset 2237 f01ac387e82b
parent 1523 7513fbe502fb
child 2469 b50b8c0eec01
equal deleted inserted replaced
2236:c7869a443b14 2237:f01ac387e82b
    67     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    67     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    68  (fn _ => [ (deepen_tac FOL_cs 0 1) ]);
    68  (fn _ => [ (deepen_tac FOL_cs 0 1) ]);
    69 
    69 
    70 use "simpdata.ML";
    70 use "simpdata.ML";
    71 
    71 
    72 use "../Pure/install_pp.ML";
    72 init_pps ();
    73 print_depth 8;
    73 print_depth 8;
    74 
    74 
    75 val FOL_build_completed = ();   (*indicate successful build*)
    75 val FOL_build_completed = ();   (*indicate successful build*)