isabelle: src/HOL/MicroJava/DFA/Semilattices.thy@01c88cf514fc (annotated)

42150 b0c0638c4aad tuned headers; wenzelm parents: 33954 diff changeset	1	(* Title: HOL/MicroJava/DFA/Semilattices.thy
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	2	Author: Gerwin Klein
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	3	Copyright 2003 TUM
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	4	*)
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	5
61361 8b5f00202e1a isabelle update_cartouches; wenzelm parents: 58886 diff changeset	6	section \<open>Semilattices\<close>
33954 1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	7
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	8	(<)
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	9	theory Semilattices
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	10	imports Err Opt Product Listn
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	11	begin
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	12
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	13	end
62390 842917225d56 more canonical names nipkow parents: 61361 diff changeset	14	(>)

author	paulson <lp15@cam.ac.uk>
	Tue, 02 May 2023 12:51:05 +0100
changeset 77934	01c88cf514fc
parent 62390	842917225d56
permissions	-rw-r--r--