Skip to content
Success

Changes

Summary

  1. bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
  2. added command 'unbundle';
Changeset 63283:a59801b7f125 by wenzelm:
bundles "finfun_syntax" and "no_finfun_syntax" for optional syntax;
The file was modified NEWS (diff)
The file was modified src/HOL/Library/FinFun.thy (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/HOL/ex/FinFunPred.thy (diff)
The file was removedsrc/HOL/Library/FinFun_Syntax.thy
Changeset 63282:7c509ddf29a5 by wenzelm:
added command 'unbundle';
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/Pure/Isar/bundle.ML (diff)
The file was modified src/Pure/Pure.thy (diff)