src/HOL/Import/HOL4Setup.thy
changeset 17801 30cbd2685e73
parent 17322 781abf7011e6
child 19064 bf19cc5a7899
equal deleted inserted replaced
17800:d39171dda84e 17801:30cbd2685e73
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     4 *)
     5 
     5 
     6 theory HOL4Setup imports MakeEqual
     6 theory HOL4Setup imports MakeEqual
     7   uses ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
     7   uses "susp.ML" "lazy_seq.ML" "lazy_scan.ML"
       
     8     ("proof_kernel.ML") ("replay.ML") ("hol4rews.ML") ("import_package.ML") begin
     8 
     9 
     9 section {* General Setup *}
    10 section {* General Setup *}
    10 
    11 
    11 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
    12 lemma eq_imp: "P = Q \<Longrightarrow> P \<longrightarrow> Q"
    12   by auto
    13   by auto