Summary
- correct (apparently untested) e1698a9578ea
- document predicator in datatypes
- derive transfer rule for predicator
- call the predicator of list list_all
The file was modified | src/Doc/Datatypes/Datatypes.thy (diff) |
The file was modified | src/Doc/Datatypes/Datatypes.thy (diff) |
The file was modified | src/HOL/BNF_Def.thy (diff) |
The file was modified | src/HOL/Tools/BNF/bnf_def.ML (diff) |
The file was modified | src/HOL/Tools/BNF/bnf_def_tactics.ML (diff) |
The file was modified | src/HOL/Tools/Transfer/transfer_bnf.ML (diff) |
The file was modified | src/Doc/Datatypes/Datatypes.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |