src/FOL/FOL.thy
changeset 13550 5a176b8dda84
parent 12367 1cee8a0db392
child 14085 8dc3e532959a
equal deleted inserted replaced
13549:f1522b892a4c 13550:5a176b8dda84
    26 setup Cla.setup
    26 setup Cla.setup
    27 setup clasetup
    27 setup clasetup
    28 
    28 
    29 use "blastdata.ML"
    29 use "blastdata.ML"
    30 setup Blast.setup
    30 setup Blast.setup
    31 use "FOL_lemmas2.ML"
    31 
       
    32 
       
    33 lemma ex1_functional: "[| EX! z. P(a,z);  P(a,b);  P(a,c) |] ==> b = c"
       
    34 by blast
       
    35 
       
    36 ML {*
       
    37 val ex1_functional = thm "ex1_functional";
       
    38 *}
    32 
    39 
    33 use "simpdata.ML"
    40 use "simpdata.ML"
    34 setup simpsetup
    41 setup simpsetup
    35 setup "Simplifier.method_setup Splitter.split_modifiers"
    42 setup "Simplifier.method_setup Splitter.split_modifiers"
    36 setup Splitter.setup
    43 setup Splitter.setup