| #
8533b4d5 |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified print modes;
more symbols;
|
| #
844a31ab |
|
30-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
28b8de30 |
|
30-Dec-2015 |
wenzelm <none@none> |
clarified print modes;
|
| #
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
| #
56730d74 |
|
06-Oct-2015 |
wenzelm <none@none> |
fewer aliases for toplevel theorem statements;
|
| #
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
| #
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
| #
ca86fe84 |
|
09-Sep-2014 |
blanchet <none@none> |
removed 'datatype_compat's that are no longer needed
|
| #
91ac5f73 |
|
09-Sep-2014 |
blanchet <none@none> |
ported HOL-Proofs-Lambda to new datatypes
|
| #
713cd402 |
|
13-Mar-2014 |
nipkow <none@none> |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
--HG--
extra : rebase_source : 4103bf02b2df95e1e84808f766f131292beef893
|
| #
aff8c6a4 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
* * *
more transition of 'xxx_rec' to 'rec_xxx' and same for case
* * *
compile
* * *
'rename_tac's to avoid referring to generated names
* * *
more robust scripts with 'rename_tac'
* * *
'where' -> 'of'
* * *
'where' -> 'of'
* * *
renamed 'xxx_rec' to 'rec_xxx'
|
| #
b11913f5 |
|
03-Dec-2012 |
blanchet <none@none> |
renamed "Type.thy" to something that's less likely to cause conflicts
--HG--
rename : src/HOL/Proofs/Lambda/Type.thy => src/HOL/Proofs/Lambda/LambdaType.thy
|