Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified signature;
  2. misc tuning;
  3. clarified demo functions;
  4. clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
Changeset 72154:2b41b710f6ef by wenzelm:
clarified signature;
The file was modified src/HOL/Eisbach/method_closure.ML (diff)
The file was modified src/HOL/Library/code_lazy.ML (diff)
The file was modified src/HOL/Library/datatype_records.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_def.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.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_lfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lift.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_util.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.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/Pure/Isar/local_theory.ML (diff)
Changeset 72153:bdbd6ff5fd0b by wenzelm:
misc tuning;
The file was modified src/Pure/Isar/local_theory.ML (diff)
Changeset 72152:3fa75db844f5 by wenzelm:
clarified demo functions;
The file was modified src/Pure/System/scala.scala (diff)
Changeset 72151:64df1e514005 by wenzelm:
clarified protocol: ML worker thread blocks and awaits result from Scala, to avoid excessive replacement threads;
The file was modified src/Pure/System/scala.ML (diff)
The file was modified src/Pure/System/scala.scala (diff)