source: src/common/FEMeasurable.ma

Revision Log Mode:


Legend:

Added
Modified
Copied or renamed
Diff Rev Age Author Log Message
(edit) @3081   7 years campbell Tidy up recent work a little.
(edit) @3063   7 years campbell Remove measure function from FEMeasurable because we're not using it …
(edit) @3032   7 years campbell Remind myself why ms_rel_normal is reasonable.
(edit) @3007   7 years campbell Sketch out how Cminor to RTLabs correctness would fit into the …
(edit) @2990   7 years campbell Replace dodgy hypothesis by nice ones, clean up a little.
(edit) @2989   7 years campbell Make front-end measurability preservation proof cope with moving the …
(edit) @2953   7 years campbell Fix silly label handling bug I realised was there during my talk…
(edit) @2727   7 years campbell Remove a couple of redundant hypotheses.
(edit) @2726   7 years campbell Show max stack preserved in FEMeasurable.
(edit) @2725   7 years campbell Add observables to FEMeasurable proof; fix silly typo.
(edit) @2690   7 years campbell Most of the measurable subtrace preservation proof done.
(edit) @2685   7 years campbell Progress on measurable trace preservation: prefix preserves observable …
(edit) @2678   7 years campbell Switch to single source step simulations for front-end measurable …
(edit) @2670   7 years campbell Clean up from recent commits.
(edit) @2669   7 years campbell Tweak exec_steps output; show that simulations extend to measurable …
(edit) @2668   7 years campbell Intermediate measurable proof check-in before I change its traces again.
(edit) @2644   7 years campbell Commit some work on FEMeasurable before trying to do something nicer …
(edit) @2618   7 years campbell Tidy up measurable a little.
(add) @2597   7 years campbell Some work in progress on measurable subtrace preservation.
Note: See TracRevisionLog for help on using the revision log.