Thomas Sewell
|
af86632985
|
Fix remaining sorries in crefine.
|
2015-07-16 14:44:56 +10:00 |
|
Thomas Sewell
|
e9180d5cb5
|
Repair refine/crefine for WCET annotations.
|
2015-07-14 14:23:29 +10:00 |
|
Thomas Sewell
|
ca4391881c
|
WIP on WCET annotations.
|
2015-07-14 14:23:29 +10:00 |
Gerwin Klein
|
eea646c84a
|
crefine: 2015 update up to Tcb_C
|
2015-05-18 09:11:43 +10:00 |
|
Gerwin Klein
|
12fa86863a
|
fewer warnings
|
2015-05-16 19:52:49 +10:00 |
David Greenaway
|
03b1952aaa
|
crefine: Port CRefine to Isabelle 2014.
|
2014-09-11 16:57:59 +10:00 |
|
Thomas Sewell
|
9b01fada15
|
Refine working.
|
2014-08-11 18:51:04 +10:00 |
|
Thomas Sewell
|
fc6e57716a
|
Proof updates, working as far as AInvs.
|
2014-08-11 14:50:56 +10:00 |
|
Gerwin Klein
|
154da63715
|
remove old levity and taint-mode comments
|
2014-07-22 18:10:28 +02:00 |
|
Gerwin Klein
|
50dda7708c
|
comment cleanup
|
2014-07-22 18:10:20 +02:00 |
|
Gerwin Klein
|
2a03e81df4
|
Import release snapshot.
|
2014-07-14 21:32:44 +02:00 |