src/HOL/Metis.thy
changeset 58889 5b7a9633cfa8
parent 58818 ee85e7b82d00
child 60758 d8d85a8172b5
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     2     Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     3     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     4     Author:     Jasmin Blanchette, TU Muenchen
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 *)
     5 *)
     6 
     6 
     7 header {* Metis Proof Method *}
     7 section {* Metis Proof Method *}
     8 
     8 
     9 theory Metis
     9 theory Metis
    10 imports ATP
    10 imports ATP
    11 begin
    11 begin
    12 
    12