src/Sequents/ILL/washing.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 16415 d4e2f121e219
permissions -rw-r--r--
converted to Isar theory format;
     1 (* $Id$ *)
     2 
     3 (* "activate" definitions for use in proof *)
     4 
     5 val changeI = [context1] RL ([change] RLN (2,[cut]));
     6 val load1I =  [context1] RL ([load1]  RLN (2,[cut]));
     7 val washI =   [context1] RL ([wash]   RLN (2,[cut]));
     8 val dryI =    [context1] RL ([dry]    RLN (2,[cut]));
     9 
    10 
    11 
    12 (* a load of dirty clothes and two dollars gives you clean clothes *)
    13 
    14 Goal "dollar , dollar , dirty |- clean";
    15 
    16 by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);
    17 
    18 
    19 (* order of premises doesn't matter *)
    20 
    21 prove_goal (the_context ()) "dollar , dirty , dollar |- clean"
    22 (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);
    23 
    24 
    25 (* alternative formulation *)
    26 
    27 prove_goal (the_context ()) "dollar , dollar |- dirty -o clean"
    28 (fn _ => [best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1]);