removed redundant "open" declarations
authorpaulson
Fri Jun 17 11:34:04 2005 +0200 (2005-06-17)
changeset 16415d4e2f121e219
parent 16414 cad2cf55c851
child 16416 6061ae1f90f2
removed redundant "open" declarations
src/Sequents/ILL/ILL_predlog.ML
src/Sequents/ILL/washing.ML
     1.1 --- a/src/Sequents/ILL/ILL_predlog.ML	Thu Jun 16 20:30:37 2005 +0200
     1.2 +++ b/src/Sequents/ILL/ILL_predlog.ML	Fri Jun 17 11:34:04 2005 +0200
     1.3 @@ -1,6 +1,3 @@
     1.4 -
     1.5 -open ILL_predlog;
     1.6 -
     1.7  
     1.8  fun auto1 x = prove_goal thy x
     1.9   (fn prems => [best_tac safe_cs 1]) ;
     2.1 --- a/src/Sequents/ILL/washing.ML	Thu Jun 16 20:30:37 2005 +0200
     2.2 +++ b/src/Sequents/ILL/washing.ML	Fri Jun 17 11:34:04 2005 +0200
     2.3 @@ -1,6 +1,3 @@
     2.4 -
     2.5 -open washing;
     2.6 -
     2.7  (* "activate" definitions for use in proof *)
     2.8  
     2.9  val changeI = [context1] RL ([change] RLN (2,[cut]));