src/Sequents/LK.thy
equal inserted replaced
17480:fd19f77dcf60 17481:75166ebb619b
`     1 (*  Title:      LK/LK`
`     1 (*  Title:      LK/LK.ML`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     4     Copyright   1993  University of Cambridge`
`     4     Copyright   1993  University of Cambridge`
`     5 `
`     5 `
`     6 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the`
`     6 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the`
`    11 `
`    11 `
`    12 CANNOT be added to LK0.thy because modal logic is built upon it, and`
`    12 CANNOT be added to LK0.thy because modal logic is built upon it, and`
`    13 various modal rules would become inconsistent.`
`    13 various modal rules would become inconsistent.`
`    14 *)`
`    14 *)`
`    15 `
`    15 `
`    16 LK = LK0 +`
`    16 theory LK`
`       `
`    17 imports LK0`
`       `
`    18 uses ("simpdata.ML")`
`       `
`    19 begin`
`    17 `
`    20 `
`    18 rules`
`    21 axioms`
`    19 `
`    22 `
`    20   monotonic  "(\$H |- P ==> \$H |- Q) ==> \$H, P |- Q"`
`    23   monotonic:  "(\$H |- P ==> \$H |- Q) ==> \$H, P |- Q"`
`    21 `
`    24 `
`    22   left_cong  "[| P == P';  |- P' ==> (\$H |- \$F) == (\$H' |- \$F') |] `
`    25   left_cong:  "[| P == P';  |- P' ==> (\$H |- \$F) == (\$H' |- \$F') |]`
`    23               ==> (P, \$H |- \$F) == (P', \$H' |- \$F')"`
`    26                ==> (P, \$H |- \$F) == (P', \$H' |- \$F')"`
`       `
`    27 `
`       `
`    28 ML {* use_legacy_bindings (the_context ()) *}`
`       `
`    29 `
`       `
`    30 use "simpdata.ML"`
`       `
`    31 `
`    24 end`
`    32 end`