#
ba266305 |
|
07-Oct-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
ba81fa63 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header;
|
#
aba785da |
|
15-Jan-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
#
c040dd23 |
|
24-Nov-2009 |
haftmann <none@none> |
backported parts of abstract byte code verifier from AFP/Jinja --HG-- extra : rebase_source : 1d943bc92831d0a92004a43f72ff37eb352bf23f
|
#
207a2493 |
|
12-Nov-2009 |
hoelzl <none@none> |
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
af3a7470 |
|
27-Mar-2008 |
wenzelm <none@none> |
avoid amiguity of State.state vs. JVMType.state;
|
#
bc65205f |
|
07-Feb-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
cc54dad0 |
|
26-May-2003 |
streckem <none@none> |
Introduced distinction wf_prog vs. ws_prog
|
#
10a62416 |
|
18-Jun-2002 |
kleing <none@none> |
LBV instantiantion refactored, streamlined
|
#
40b52446 |
|
14-Jun-2002 |
kleing <none@none> |
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
|
#
f7fa2b3a |
|
02-Apr-2002 |
nipkow <none@none> |
Started to convert to locales
|
#
64369aa5 |
|
24-Mar-2002 |
kleing <none@none> |
tuned
|
#
129ca3f7 |
|
24-Mar-2002 |
kleing <none@none> |
cleanup + simpler monotonicity
|
#
d2589390 |
|
03-Mar-2002 |
kleing <none@none> |
symbolized
|
#
6c89dca9 |
|
26-Feb-2002 |
kleing <none@none> |
introduces SystemClasses and BVExample
|
#
0e7365d8 |
|
21-Feb-2002 |
kleing <none@none> |
new document
|
#
1757b3b6 |
|
15-Dec-2001 |
kleing <none@none> |
exceptions
|
#
e67da82d |
|
16-Nov-2001 |
kleing <none@none> |
fixed maxs bug
|
#
6ddaa347 |
|
05-Oct-2001 |
wenzelm <none@none> |
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat, "num" syntax (still with "#"), Numeral0, Numeral1;
|
#
316a7879 |
|
15-May-2001 |
nipkow <none@none> |
welltyping -> wt_step
|
#
e20de190 |
|
14-May-2001 |
nipkow <none@none> |
simplified defs and proofs a little
|
#
154c20da |
|
28-Mar-2001 |
nipkow <none@none> |
Got rid of is_dfa
|
#
63898fc2 |
|
27-Feb-2001 |
nipkow <none@none> |
*** empty log message ***
|
#
ef8f4a2b |
|
14-Jan-2001 |
kleing <none@none> |
removed instructions Aconst_null+Bipush, introduced LitPush
|
#
9a40d08d |
|
09-Jan-2001 |
nipkow <none@none> |
*** empty log message ***
|
#
68ccecef |
|
07-Jan-2001 |
kleing <none@none> |
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
|
#
cb91f07d |
|
13-Dec-2000 |
kleing <none@none> |
removed sorry proof
|
#
c3bcab57 |
|
12-Dec-2000 |
kleing <none@none> |
completeness (unfinished)
|
#
2e481a7e |
|
10-Dec-2000 |
kleing <none@none> |
kildall ==> wt_method for whole program
|
#
7c1cbc47 |
|
07-Dec-2000 |
kleing <none@none> |
updated for is_class changes
|
#
342e0951 |
|
06-Dec-2000 |
oheimb <none@none> |
improved superclass entry for classes and definition status of is_class, class corrected recursive definitions of "method" and "fields" Beware: some proofs are incomplete (sorry, oops), preliminary comments with DvO:
|
#
5934a31a |
|
05-Dec-2000 |
kleing <none@none> |
BCV Integration
|