src/FOL/ROOT.ML
changeset 731 435ff9ec4058
parent 666 4d9f6d83c2bf
child 1004 70676af0ac97
equal deleted inserted replaced
730:15c822377c18 731:435ff9ec4058
    62 val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
    62 val FOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
    63                      addSEs [exE,ex1E] addEs [allE];
    63                      addSEs [exE,ex1E] addEs [allE];
    64 
    64 
    65 val ex1_functional = prove_goal FOL.thy
    65 val ex1_functional = prove_goal FOL.thy
    66     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    66     "!!a b c. [| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
    67  (fn _ => [ (deepen_tac FOL_cs 1 1) ]);
    67  (fn _ => [ (deepen_tac FOL_cs 0 1) ]);
    68 
    68 
    69 use "simpdata.ML";
    69 use "simpdata.ML";
    70 
    70 
    71 use "../Pure/install_pp.ML";
    71 use "../Pure/install_pp.ML";
    72 print_depth 8;
    72 print_depth 8;