Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. merged
  2. tuned whitespace;
  3. more symbols;
  4. profer bundle lattice_syntax;
  5. prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended;
Changeset 12372:c1393433f082 by wenzelm:
merged
Changeset 12371:6ef2e075a034 by wenzelm:
tuned whitespace;
The file was modified thys/ZFC_in_HOL/ZFC_Cardinals.thy
The file was modified thys/ZFC_in_HOL/ZFC_in_HOL.thy
Changeset 12370:6136280343a0 by wenzelm:
more symbols;
The file was modified thys/ZFC_in_HOL/Kirby.thy
The file was modified thys/ZFC_in_HOL/Ordinal_Exp.thy
The file was modified thys/ZFC_in_HOL/ZFC_Cardinals.thy
The file was modified thys/ZFC_in_HOL/ZFC_in_HOL.thy
Changeset 12369:e5dd226cebfc by wenzelm:
profer bundle lattice_syntax;
The file was modified thys/ZFC_in_HOL/ZFC_in_HOL.thy
Changeset 12368:8cb75b461233 by wenzelm:
prefer existing lattice_syntax and no_lattice_syntax, with proper 'no_notation' as intended;
The file was modified thys/Complex_Bounded_Operators/Cblinfun_Code.thy
The file was modified thys/Complex_Bounded_Operators/Cblinfun_Code_Examples.thy
The file was modified thys/Complex_Bounded_Operators/Complex_Bounded_Linear_Function.thy
The file was modified thys/Complex_Bounded_Operators/Complex_L2.thy
The file was modified thys/Complex_Bounded_Operators/Complex_Vector_Spaces.thy
The file was modified thys/Complex_Bounded_Operators/extra/Extra_Lattice.thy
The file was modified thys/Registers/Quantum_Extra.thy