2010-11-21 | Christian Urban | added example Foo2.thy | file | diff | annotate |
2010-11-15 | Christian Urban | tuned example | file | diff | annotate |
2010-11-15 | Christian Urban | proved that bn functions return a finite set | file | diff | annotate |
2010-11-14 | Christian Urban | tuned example | file | diff | annotate |
2010-11-13 | Christian Urban | lifted permute_bn constants | file | diff | annotate |
2010-11-13 | Christian Urban | respectfulness for permute_bn functions | file | diff | annotate |
2010-11-12 | Christian Urban | automated permute_bn functions (raw ones first) | file | diff | annotate |
2010-11-10 | Christian Urban | adapted to changes by Florian on the quotient package and removed local fix for function package | file | diff | annotate |
2010-09-29 | Christian Urban | simplified exhaust proofs | file | diff | annotate |
2010-09-29 | Christian Urban | worked example Foo1 with induct_schema | file | diff | annotate |
2010-09-28 | Christian Urban | added Foo1 to explore a contrived example | file | diff | annotate |