Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. use Item_Net to store inductive info
Changeset 65412:da25458453e3 by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 65411:3c628937899d by lars hupel _lars.hupel@mytum.de_:
use Item_Net to store inductive info
The file was modified src/HOL/Library/Countable.thy (diff)
The file was modified src/HOL/Nominal/nominal_inductive.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive2.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/core_data.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_realizer.ML (diff)