Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper concept of code declaration wrt. atomicity and Isar declarations
  2. merged
  3. complete on long name components as well;
  4. added command 'alias' and 'type_alias';
  5. tuned;
  6. tuned signature;
  7. unused;
  8. qualify Complete_Partial_Order2.compact
Changeset 66251:cd935b7cb3fb by haftmann:
proper concept of code declaration wrt. atomicity and Isar declarations
The file was modified src/Doc/Codegen/Further.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Candidates.thy (diff)
The file was modified src/HOL/Codegenerator_Test/Generate.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/Mapping.thy (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Predicate.thy (diff)
The file was modified src/HOL/Product_Type.thy (diff)
The file was modified src/HOL/String.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_compat.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_setup.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_primrec.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_rep_datatype.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_size.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/random_generators.ML (diff)
The file was modified src/HOL/Tools/code_evaluation.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 66250:56a87a5093be by wenzelm:
merged
Changeset 66249:f50e6e31a0ee by wenzelm:
complete on long name components as well;
The file was modified src/Pure/General/name_space.ML (diff)
Changeset 66248:df85956228c2 by wenzelm:
added command 'alias' and 'type_alias';
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/HOL/BNF_Greatest_Fixpoint.thy (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Pure.thy (diff)
Changeset 66247:8d966b4a7469 by wenzelm:
tuned;
The file was modified src/Pure/General/name_space.ML (diff)
Changeset 66246:c2c18b6b48da by wenzelm:
tuned signature;
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
Changeset 66245:da3b0e848182 by wenzelm:
unused;
The file was modified src/Pure/Isar/local_theory.ML (diff)
The file was modified src/Pure/Isar/proof_context.ML (diff)
The file was modified src/Pure/sign.ML (diff)
The file was modified src/Pure/type.ML (diff)
Changeset 66244:4c999b5d78e2 by Andreas Lochbihler:
qualify Complete_Partial_Order2.compact
The file was modified src/HOL/Library/Complete_Partial_Order2.thy (diff)