src/Pure/Isar/proof_context.ML
changeset 34969 7b8c366e34a2
parent 33956 e9afca2118d4
child 35114 18cd034922ba
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Feb 01 14:12:12 2010 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Feb 02 11:38:38 2010 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
     1.5    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
     1.6    val facts_of: Proof.context -> Facts.T
     1.7 +  val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
     1.8    val transfer_syntax: theory -> Proof.context -> Proof.context
     1.9    val transfer: theory -> Proof.context -> Proof.context
    1.10    val theory: (theory -> theory) -> Proof.context -> Proof.context