isabelle: src/HOL/MicroJava/DFA/Abstract_BV.thy@32903b99c2ef (annotated)

42150 b0c0638c4aad tuned headers; wenzelm parents: 33954 diff changeset	1	(* Title: HOL/MicroJava/DFA/Abstract_BV.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
58886 8a6cac7c7247 modernized header; wenzelm parents: 42150 diff changeset	6	section {* Abstract Bytecode Verifier *}
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 Abstract_BV
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	10	imports Typing_Framework_err Kildall LBVCorrect LBVComplete
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
1bc3b688548c backported parts of abstract byte code verifier from AFP/Jinja haftmann parents: diff changeset	14	(>)

author	wenzelm
	Sat, 03 Jan 2015 20:28:53 +0100
changeset 59246	32903b99c2ef
parent 58886	8a6cac7c7247
child 61361	8b5f00202e1a
permissions	-rw-r--r--