isabelle: src/HOLCF/Porder0.thy@a2c34e6ca4f8 (annotated)

2640 ee4dfce170a0 Changes of HOLCF from Oscar Slotosch: slotosch parents: 2394 diff changeset	1	(* Title: HOLCF/Porder0.thy
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	2	ID: $Id$
1479 21eb5e156d91 expanded tabs clasohm parents: 1274 diff changeset	3	Author: Franz Regensburger
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	4
12030 46d57d0290a2 GPLed; wenzelm parents: 7661 diff changeset	5	Definition of class porder (partial order).
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	6	*)
3a0485439396 structural induction for strict lists nipkow parents: diff changeset	7
7661 8c3190b173aa depend on Main; wenzelm parents: 3323 diff changeset	8	Porder0 = Main +
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	9
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	10	(* introduce a (syntactic) class for the constant << *)
12338 de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type"); wenzelm parents: 12114 diff changeset	11	axclass sq_ord < type
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	12
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	13	(* characteristic constant << for po *)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	14	consts
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	15	"<<" :: "['a,'a::sq_ord] => bool" (infixl 55)
2394 91d8abf108be adaptions for symbol font oheimb parents: 2291 diff changeset	16
12114 a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead; wenzelm parents: 12030 diff changeset	17	syntax (xsymbols)
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	18	"op <<" :: "['a,'a::sq_ord] => bool" (infixl "\\<sqsubseteq>" 55)
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	19
3323 194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	20	axclass po < sq_ord
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	21	(* class axioms: *)
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	22	refl_less "x << x"
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	23	antisym_less "[\|x << y; y << x \|] ==> x = y"
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	24	trans_less "[\|x << y; y << z \|] ==> x << z"
194ae2e0c193 eliminated the constant less by the introduction of the axclass sq_ord slotosch parents: 3310 diff changeset	25
298 3a0485439396 structural induction for strict lists nipkow parents: diff changeset	26	end
1274 ea0668a1c0ba added 8bit pragmas regensbu parents: 442 diff changeset	27
ea0668a1c0ba added 8bit pragmas regensbu parents: 442 diff changeset	28

author	berghofe
	Fri, 10 Dec 2004 16:48:01 +0100
changeset 15394	a2c34e6ca4f8
parent 14981	e73f8140af78
child 15562	8455c9671494
permissions	-rw-r--r--