src/Sequents/LK/Propositional.thy
changeset 41959 b460124855b8
parent 35762 af3ff2ba4c54
child 55229 08f2ebb65078
equal deleted inserted replaced
41958:5abc60a017e0 41959:b460124855b8
     1 (*  Title:      LK/Propositional.thy
     1 (*  Title:      Sequents/LK/Propositional.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1992  University of Cambridge
     3     Copyright   1992  University of Cambridge
     4 *)
     4 *)
     5 
     5 
     6 header {* Classical sequent calculus: examples with propositional connectives *}
     6 header {* Classical sequent calculus: examples with propositional connectives *}