src/Sequents/LK.thy
changeset 21428 f84cf8e9cad8
parent 17481 75166ebb619b
child 27149 123377499a8e
equal deleted inserted replaced
21427:7c8f4a331f9b 21428:f84cf8e9cad8
    23   monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    23   monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q"
    24 
    24 
    25   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    25   left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
    26                ==> (P, $H |- $F) == (P', $H' |- $F')"
    26                ==> (P, $H |- $F) == (P', $H' |- $F')"
    27 
    27 
    28 ML {* use_legacy_bindings (the_context ()) *}
       
    29 
       
    30 use "simpdata.ML"
    28 use "simpdata.ML"
    31 
    29 
    32 end
    30 end