src/HOL/Tools/Function/pat_completeness.ML
changeset 47432 e1576d13e933
parent 47060 e2741ec9ae36
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/Function/pat_completeness.ML	Thu Apr 12 11:34:50 2012 +0200
     1.2 +++ b/src/HOL/Tools/Function/pat_completeness.ML	Thu Apr 12 18:39:19 2012 +0200
     1.3 @@ -7,11 +7,8 @@
     1.4  signature PAT_COMPLETENESS =
     1.5  sig
     1.6      val pat_completeness_tac: Proof.context -> int -> tactic
     1.7 -    val pat_completeness: Proof.context -> Proof.method
     1.8      val prove_completeness : theory -> term list -> term -> term list list ->
     1.9        term list list -> thm
    1.10 -
    1.11 -    val setup : theory -> theory
    1.12  end
    1.13  
    1.14  structure Pat_Completeness : PAT_COMPLETENESS =
    1.15 @@ -153,11 +150,4 @@
    1.16    end
    1.17    handle COMPLETENESS => no_tac)
    1.18  
    1.19 -
    1.20 -val pat_completeness = SIMPLE_METHOD' o pat_completeness_tac
    1.21 -
    1.22 -val setup =
    1.23 -  Method.setup @{binding pat_completeness} (Scan.succeed pat_completeness)
    1.24 -    "Completeness prover for datatype patterns"
    1.25 -
    1.26  end