src/HOL/Nominal/Examples/W.thy
author wenzelm
Sat, 09 Aug 2008 22:43:53 +0200
changeset 27811 44bc67675210
parent 26195 8292f8723e99
child 28655 2822c56dd1cf
permissions -rw-r--r--
unified Args.T with OuterLex.token; moved datatype value/slot and basic operations to outer_lex.ML; removed unused terminator; removed obsolete !!!, position, nat, int, list(1), enum(1) and_list(1) (cf. outer_parse.ML); removed obsolete thm_sel (cf. attrib.ML); one unified version of parse/parse1 (formerly arguments/generic_args1 in outer_parse.ML);
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