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