isabelle: src/HOL/Lex/Prefix.thy@63e53327f5e5 (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1344 diff changeset	1	(* Title: HOL/Lex/Prefix.thy
1344 f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1344 diff changeset	3	Author: Tobias Nipkow
1344 f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	4	Copyright 1995 TUM
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	5	*)
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	6
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	7	Prefix = List +
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	8
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	9	arities list :: (term)ord
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	10
f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	11	defs
6675 63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation paulson parents: 1476 diff changeset	12	prefix_def "xs <= zs == ? ys. zs = xs@ys"
63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation paulson parents: 1476 diff changeset	13
63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation paulson parents: 1476 diff changeset	14	strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)"
63e53327f5e5 changes to show that Lists are partially ordered by the prefix relation paulson parents: 1476 diff changeset	15
1344 f172a7f14e49 Half a lexical analyzer generator. nipkow parents: diff changeset	16	end

author	paulson
	Fri, 21 May 1999 10:50:04 +0200
changeset 6675	63e53327f5e5
parent 1476	608483c2122a
child 8523	7ffc94f2f42d
permissions	-rw-r--r--