isabelle: src/HOL/Lex/Prefix.thy@50ec59aff389 (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
9156 b9fe44ad3381 replaced arities by instance; wenzelm parents: 8523 diff changeset	9	instance list :: (term)ord
1344 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	wenzelm
	Wed, 02 Aug 2000 19:40:14 +0200
changeset 9502	50ec59aff389
parent 9156	b9fe44ad3381
permissions	-rw-r--r--