src/Sequents/ILL/washing.thy
changeset 17481 75166ebb619b
parent 6252 935f183bf406
     1.1 --- a/src/Sequents/ILL/washing.thy	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/ILL/washing.thy	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -1,33 +1,38 @@
     1.4 -
     1.5  
     1.6 -(* code by Sara Kalvala, based on Paulson's LK 
     1.7 +(* $Id$ *)
     1.8 +
     1.9 +(* code by Sara Kalvala, based on Paulson's LK
    1.10                             and Moore's tisl.ML *)
    1.11  
    1.12 -washing = ILL +
    1.13 +theory washing
    1.14 +imports ILL
    1.15 +begin
    1.16  
    1.17  consts
    1.18 -
    1.19 -dollar,quarter,loaded,dirty,wet,clean        :: "o"			
    1.20 +  dollar :: o
    1.21 +  quarter :: o
    1.22 +  loaded :: o
    1.23 +  dirty :: o
    1.24 +  wet :: o
    1.25 +  clean :: o
    1.26  
    1.27 -  
    1.28 -rules
    1.29 -
    1.30 -
    1.31 -  change
    1.32 +axioms
    1.33 +  change:
    1.34    "dollar |- (quarter >< quarter >< quarter >< quarter)"
    1.35  
    1.36 -  load1
    1.37 +  load1:
    1.38    "quarter , quarter , quarter , quarter , quarter |- loaded"
    1.39  
    1.40 -  load2
    1.41 +  load2:
    1.42    "dollar , quarter |- loaded"
    1.43  
    1.44 -  wash
    1.45 +  wash:
    1.46    "loaded , dirty |- wet"
    1.47  
    1.48 -  dry
    1.49 +  dry:
    1.50    "wet, quarter , quarter , quarter |- clean"
    1.51  
    1.52 +ML {* use_legacy_bindings (the_context ()) *}
    1.53 +
    1.54  end
    1.55  
    1.56 -  
    1.57 \ No newline at end of file