src/HOL/Nominal/Examples/W.thy
author wenzelm
Mon, 14 Apr 2008 21:44:53 +0200
changeset 26647 147c920ed5f7
parent 26195 8292f8723e99
child 28655 2822c56dd1cf
permissions -rw-r--r--
avoid duplicate fact bindings;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26195
8292f8723e99 added new example
urbanc
parents:
diff changeset
     1
(* "$Id$" *)
8292f8723e99 added new example
urbanc
parents:
diff changeset
     2
8292f8723e99 added new example
urbanc
parents:
diff changeset
     3
theory W
8292f8723e99 added new example
urbanc
parents:
diff changeset
     4
imports "Nominal"
8292f8723e99 added new example
urbanc
parents:
diff changeset
     5
begin
8292f8723e99 added new example
urbanc
parents:
diff changeset
     6
8292f8723e99 added new example
urbanc
parents:
diff changeset
     7
text {* stub until a cleaned-up version will appear here *}
8292f8723e99 added new example
urbanc
parents:
diff changeset
     8
8292f8723e99 added new example
urbanc
parents:
diff changeset
     9
end