summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | smolkas |

Wed, 02 Jan 2013 20:53:01 +0100 | |

changeset 50680 | adbbe04b7c75 |

parent 50679 | e409d9f8ec75 |

child 50692 | 97f951edca46 |

removed old, unused code

--- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Jan 02 20:52:39 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Jan 02 20:53:01 2013 +0100 @@ -41,7 +41,6 @@ val direct_graph : direct_sequent list -> direct_graph val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof val succedent_of_cases : (clause * direct_inference list) list -> clause - val chain_direct_proof : direct_proof -> direct_proof val string_of_direct_proof : direct_proof -> string end; @@ -186,19 +185,6 @@ in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end in redirect [] axioms seqs end -val chain_direct_proof = - let - fun chain_inf cl0 (seq as Have (cs, c)) = - seq - | chain_inf _ (Cases cases) = Cases (map chain_case cases) - and chain_case (c, is) = (c, chain_proof (SOME c) is) - and chain_proof _ [] = [] - | chain_proof (SOME prev) (i :: is) = - chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is - | chain_proof _ (i :: is) = - i :: chain_proof (SOME (succedent_of_inference i)) is - in chain_proof NONE end - fun indent 0 = "" | indent n = " " ^ indent (n - 1)