src/Sequents/ILL/washing.thy
changeset 6252 935f183bf406
child 17481 75166ebb619b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Sequents/ILL/washing.thy	Fri Feb 05 21:14:17 1999 +0100
     1.3 @@ -0,0 +1,33 @@
     1.4 +
     1.5 +
     1.6 +(* code by Sara Kalvala, based on Paulson's LK 
     1.7 +                           and Moore's tisl.ML *)
     1.8 +
     1.9 +washing = ILL +
    1.10 +
    1.11 +consts
    1.12 +
    1.13 +dollar,quarter,loaded,dirty,wet,clean        :: "o"			
    1.14 +
    1.15 +  
    1.16 +rules
    1.17 +
    1.18 +
    1.19 +  change
    1.20 +  "dollar |- (quarter >< quarter >< quarter >< quarter)"
    1.21 +
    1.22 +  load1
    1.23 +  "quarter , quarter , quarter , quarter , quarter |- loaded"
    1.24 +
    1.25 +  load2
    1.26 +  "dollar , quarter |- loaded"
    1.27 +
    1.28 +  wash
    1.29 +  "loaded , dirty |- wet"
    1.30 +
    1.31 +  dry
    1.32 +  "wet, quarter , quarter , quarter |- clean"
    1.33 +
    1.34 +end
    1.35 +
    1.36 +  
    1.37 \ No newline at end of file