src/HOL/Nominal/Examples/W.thy
author berghofe
Thu, 03 Apr 2008 17:52:51 +0200
changeset 26533 aeef55a3d1d5
parent 26195 8292f8723e99
child 28655 2822c56dd1cf
permissions -rw-r--r--
Deleted code for axiomatic introduction of datatypes. Instead, the package now uses SkipProof.prove rather than Goal.prove to do proofs.
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