equal
deleted
inserted
replaced
71 val proof_data_of: theory -> string list |
71 val proof_data_of: theory -> string list |
72 (*generic context*) |
72 (*generic context*) |
73 datatype generic = Theory of theory | Proof of proof |
73 datatype generic = Theory of theory | Proof of proof |
74 val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a |
74 val cases: (theory -> 'a) -> (proof -> 'a) -> generic -> 'a |
75 val mapping: (theory -> theory) -> (proof -> proof) -> generic -> generic |
75 val mapping: (theory -> theory) -> (proof -> proof) -> generic -> generic |
|
76 val mapping_result: (theory -> 'a * theory) -> (proof -> 'a * proof) -> generic -> 'a * generic |
76 val the_theory: generic -> theory |
77 val the_theory: generic -> theory |
77 val the_proof: generic -> proof |
78 val the_proof: generic -> proof |
78 val map_theory: (theory -> theory) -> generic -> generic |
79 val map_theory: (theory -> theory) -> generic -> generic |
79 val map_proof: (proof -> proof) -> generic -> generic |
80 val map_proof: (proof -> proof) -> generic -> generic |
80 val theory_map: (generic -> generic) -> theory -> theory |
81 val theory_map: (generic -> generic) -> theory -> theory |
580 |
581 |
581 fun cases f _ (Theory thy) = f thy |
582 fun cases f _ (Theory thy) = f thy |
582 | cases _ g (Proof prf) = g prf; |
583 | cases _ g (Proof prf) = g prf; |
583 |
584 |
584 fun mapping f g = cases (Theory o f) (Proof o g); |
585 fun mapping f g = cases (Theory o f) (Proof o g); |
|
586 fun mapping_result f g = cases (apsnd Theory o f) (apsnd Proof o g); |
585 |
587 |
586 val the_theory = cases I (fn _ => raise Fail "Ill-typed context: theory expected"); |
588 val the_theory = cases I (fn _ => raise Fail "Ill-typed context: theory expected"); |
587 val the_proof = cases (fn _ => raise Fail "Ill-typed context: proof expected") I; |
589 val the_proof = cases (fn _ => raise Fail "Ill-typed context: proof expected") I; |
588 |
590 |
589 fun map_theory f = Theory o f o the_theory; |
591 fun map_theory f = Theory o f o the_theory; |