Commits · 03d40a28d1e8306f7874ad403f34bfe555179c05 · AVA / FloVer

12 Oct, 2016 1 commit
- Add Unary operators to expression semantics · 129566e2
  Heiko Becker authored Oct 12, 2016
  
  129566e2
06 Oct, 2016 1 commit
- Add 2 to 3 line comment to every file to explain where it is used and what it... · 953cceba
  Heiko Becker authored Oct 06, 2016
```
Add 2 to 3 line comment to every file to explain where it is used and what it contains. Add references to paper where possible
```
  953cceba
18 Sep, 2016 2 commits
- Add equality on booleans for expressions · b8cdcecd
  Heiko Becker authored Sep 18, 2016
  
  b8cdcecd
- More cleanup. Make external dependencies explicit · 62fa1565
  Heiko Becker authored Sep 18, 2016
  
  62fa1565
26 Aug, 2016 3 commits
- Type in doc fixing and add lemma existential_rewriting to HOL dev, without proof · 10c11261
  Heiko Becker authored Aug 26, 2016
  
  10c11261
- Make eval_0_det proper proof in HOL-Light style and simplify coq dev · c42a6ab3
  Heiko Becker authored Aug 26, 2016
  
  c42a6ab3
- Move machineEpsilon to Infra.RealSimps · 692353f0
  Heiko Becker authored Aug 26, 2016
  
  692353f0
23 Aug, 2016 1 commit
- Minor lemma fixes · 9251741e
  Heiko Becker authored Aug 23, 2016
  
  9251741e
22 Aug, 2016 2 commits
- Addition correct apart from correctness hole for IV checker · a54517e0
  Heiko Becker authored Aug 22, 2016
  
  a54517e0
- Prove existential rewriting lemma for evaluations · 687917a3
  Heiko Becker authored Aug 22, 2016
  
  687917a3
20 Aug, 2016 1 commit
- Make a little cleanup · 72273a09
  Heiko Becker authored Aug 20, 2016
  
  72273a09
18 Aug, 2016 1 commit
- Fix requires after refactoring · e8dd12b6
  Heiko Becker authored Aug 18, 2016
  
  e8dd12b6
17 Aug, 2016 1 commit
- Simplify Coq proof · 372a1de9
  Heiko Becker authored Aug 17, 2016
  
  372a1de9
16 Aug, 2016 2 commits
- Toy example proven with holes, these should be formally showing some... · ad2b04ee
  Heiko Becker authored Aug 16, 2016
```
Toy example proven with holes, these should be formally showing some transitivity rules and upper bounds
```
  ad2b04ee
- Add lemma about parameters, fix flaw that parameters had no error bound · 67f24a94
  Heiko Becker authored Aug 16, 2016
  
  67f24a94
15 Aug, 2016 1 commit
- Big cleanup in Coq dev · e1c27762
  Heiko Becker authored Aug 15, 2016
  
  e1c27762
12 Aug, 2016 3 commits
- Draft lemma on variables · 43840665
  Heiko Becker authored Aug 12, 2016
  
  43840665
- general lemma about constants · a13cdb39
  Heiko Becker authored Aug 12, 2016
  
  a13cdb39
- Fix some annoying definitions · 2b45e6a8
  Heiko Becker authored Aug 12, 2016
  
  2b45e6a8
11 Aug, 2016 2 commits
- Fix machine epsilon in expressions · 64097c88
  Heiko Becker authored Aug 11, 2016
  
  64097c88
- Try to prove copnstant case, fix machine epsilon. Still not working... · 176780f1
  Heiko Becker authored Aug 11, 2016
  
  176780f1
10 Aug, 2016 1 commit
- Add real machine epsilon from daisy · 4795737c
  Heiko Becker authored Aug 10, 2016
  
  4795737c
01 Jul, 2016 1 commit
- Add type abbrev for environments · e892d8de
  Heiko Becker authored Jul 01, 2016
  
  e892d8de
30 Jun, 2016 1 commit
- Prove exp eval deterministic in coq, prove side-lemma in HOL · 6144c6f9
  Heiko Becker authored Jun 30, 2016
  
  6144c6f9
29 Jun, 2016 1 commit
- Start working on toy example proof, add coq definitions · 3e046357
  Heiko Becker authored Jun 29, 2016
  
  3e046357