| #
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
|