isabelle: src/HOL/Lex/Prefix.thy@b03a0b219139 (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
8523 7ffc94f2f42d now based on "Main", as it should be paulson parents: 6675 diff changeset	7	Prefix = Main +
1344 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 Apr 2000 11:28:18 +0200
changeset 8756	b03a0b219139
parent 8523	7ffc94f2f42d
child 9156	b9fe44ad3381
permissions	-rw-r--r--