src/Sequents/ILL/washing.thy
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 6252 935f183bf406
permissions -rw-r--r--
converted to Isar theory format;
     1 
     2 (* $Id$ *)
     3 
     4 (* code by Sara Kalvala, based on Paulson's LK
     5                            and Moore's tisl.ML *)
     6 
     7 theory washing
     8 imports ILL
     9 begin
    10 
    11 consts
    12   dollar :: o
    13   quarter :: o
    14   loaded :: o
    15   dirty :: o
    16   wet :: o
    17   clean :: o
    18 
    19 axioms
    20   change:
    21   "dollar |- (quarter >< quarter >< quarter >< quarter)"
    22 
    23   load1:
    24   "quarter , quarter , quarter , quarter , quarter |- loaded"
    25 
    26   load2:
    27   "dollar , quarter |- loaded"
    28 
    29   wash:
    30   "loaded , dirty |- wet"
    31 
    32   dry:
    33   "wet, quarter , quarter , quarter |- clean"
    34 
    35 ML {* use_legacy_bindings (the_context ()) *}
    36 
    37 end
    38