src/HOL/Tools/ATP/atp_translate.ML
changeset 44783 3634c6dba23f
parent 44782 ba4c0205267f
child 44785 f4975fa4a2f8
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:16 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Sep 07 13:50:17 2011 +0200
     1.3 @@ -16,8 +16,7 @@
     1.4    type 'a problem = 'a ATP_Problem.problem
     1.5  
     1.6    datatype locality =
     1.7 -    General | Helper | Induction | Extensionality | Intro | Elim | Simp |
     1.8 -    Local | Assum | Chained
     1.9 +    General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
    1.10  
    1.11    datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    1.12    datatype soundness = Sound_Modulo_Infiniteness | Sound
    1.13 @@ -526,8 +525,7 @@
    1.14      in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
    1.15  
    1.16  datatype locality =
    1.17 -  General | Helper | Induction | Extensionality | Intro | Elim | Simp |
    1.18 -  Local | Assum | Chained
    1.19 +  General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained
    1.20  
    1.21  datatype order = First_Order | Higher_Order
    1.22  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic