Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. clarified bindings;
  2. clarified bindings;
  3. prefer binding over base name;
  4. clarified signature;
  5. removed pointless check (see Type_Infer.object_logic);
  6. prefer precise names for internal construction;
Changeset 63006:89d19aa73081 by wenzelm:
clarified bindings;
The file was modified src/HOL/HOLCF/Tools/Domain/domain_induction.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_set.ML (diff)
The file was modified src/Pure/General/binding.ML (diff)
Changeset 63005:d743bb1b6c23 by wenzelm:
clarified bindings;
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
The file was modified src/HOL/Tools/Function/function_core.ML (diff)
The file was modified src/HOL/Tools/Function/function_lib.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
Changeset 63004:f507e6fe1d77 by wenzelm:
prefer binding over base name;
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
The file was modified src/HOL/Tools/Function/function_core.ML (diff)
The file was modified src/HOL/Tools/Function/mutual.ML (diff)
Changeset 63003:bf5fcc65586b by wenzelm:
clarified signature;
The file was modified src/HOL/HOLCF/Tools/Domain/domain_axioms.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_constructors.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_induction.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_bnf.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer_bnf.ML (diff)
The file was modified src/HOL/Tools/typedef.ML (diff)
The file was modified src/Pure/General/binding.ML (diff)
The file was modified src/Pure/General/name_space.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
Changeset 63002:56cf1249ee20 by wenzelm:
removed pointless check (see Type_Infer.object_logic);
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
Changeset 63001:637ed69b4d46 by wenzelm:
prefer precise names for internal construction;
The file was modified src/HOL/Tools/Function/function_core.ML (diff)