src/FOL/IFOL.thy
changeset 15481 fc075ae929e4
parent 15377 3d99eea28a9b
child 16019 0e1405402d53
     1.1 --- a/src/FOL/IFOL.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -5,8 +5,10 @@
     1.4  
     1.5  header {* Intuitionistic first-order logic *}
     1.6  
     1.7 -theory IFOL = Pure
     1.8 -files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"):
     1.9 +theory IFOL
    1.10 +imports Pure
    1.11 +files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
    1.12 +begin
    1.13  
    1.14  
    1.15  subsection {* Syntax and axiomatic basis *}
    1.16 @@ -268,8 +270,6 @@
    1.17    mp
    1.18    trans
    1.19  
    1.20 -
    1.21 -
    1.22  subsection {* ``Let'' declarations *}
    1.23  
    1.24  nonterminals letbinds letbind