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;
wenzelm@6252
     1
wenzelm@17481
     2
(* $Id$ *)
wenzelm@17481
     3
wenzelm@17481
     4
(* code by Sara Kalvala, based on Paulson's LK
wenzelm@6252
     5
                           and Moore's tisl.ML *)
wenzelm@6252
     6
wenzelm@17481
     7
theory washing
wenzelm@17481
     8
imports ILL
wenzelm@17481
     9
begin
wenzelm@6252
    10
wenzelm@6252
    11
consts
wenzelm@17481
    12
  dollar :: o
wenzelm@17481
    13
  quarter :: o
wenzelm@17481
    14
  loaded :: o
wenzelm@17481
    15
  dirty :: o
wenzelm@17481
    16
  wet :: o
wenzelm@17481
    17
  clean :: o
wenzelm@6252
    18
wenzelm@17481
    19
axioms
wenzelm@17481
    20
  change:
wenzelm@6252
    21
  "dollar |- (quarter >< quarter >< quarter >< quarter)"
wenzelm@6252
    22
wenzelm@17481
    23
  load1:
wenzelm@6252
    24
  "quarter , quarter , quarter , quarter , quarter |- loaded"
wenzelm@6252
    25
wenzelm@17481
    26
  load2:
wenzelm@6252
    27
  "dollar , quarter |- loaded"
wenzelm@6252
    28
wenzelm@17481
    29
  wash:
wenzelm@6252
    30
  "loaded , dirty |- wet"
wenzelm@6252
    31
wenzelm@17481
    32
  dry:
wenzelm@6252
    33
  "wet, quarter , quarter , quarter |- clean"
wenzelm@6252
    34
wenzelm@17481
    35
ML {* use_legacy_bindings (the_context ()) *}
wenzelm@17481
    36
wenzelm@6252
    37
end
wenzelm@6252
    38