src/Sequents/ILL/washing.ML
changeset 17481 75166ebb619b
parent 16415 d4e2f121e219
     1.1 --- a/src/Sequents/ILL/washing.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/ILL/washing.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,3 +1,5 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6  (* "activate" definitions for use in proof *)
     1.7  
     1.8  val changeI = [context1] RL ([change] RLN (2,[cut]));
     1.9 @@ -16,15 +18,11 @@
    1.10  
    1.11  (* order of premises doesn't matter *)
    1.12  
    1.13 -prove_goal thy "dollar , dirty , dollar |- clean"
    1.14 +prove_goal (the_context ()) "dollar , dirty , dollar |- clean"
    1.15  (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    1.16  
    1.17  
    1.18  (* alternative formulation *)
    1.19  
    1.20 -prove_goal thy "dollar , dollar |- dirty -o clean"
    1.21 +prove_goal (the_context ()) "dollar , dollar |- dirty -o clean"
    1.22  (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    1.23 -
    1.24 -
    1.25 -
    1.26 -