Z_Toolkit

This is an implementation of the Z mathematical toolkit in Isabelle/HOL, as described in ISO 13568:2002.

Name		Name	Last commit message	Last commit date
Latest commit History 164 Commits
.github/workflows		.github/workflows
document		document
symbols		symbols
.gitignore		.gitignore
Action_Command.thy		Action_Command.thy
Bounded_List.thy		Bounded_List.thy
Channels_Events.thy		Channels_Events.thy
Countable_Set_Extra.thy		Countable_Set_Extra.thy
Def_Const.thy		Def_Const.thy
Enum_Type.ML		Enum_Type.ML
Enum_Type.thy		Enum_Type.thy
FSet_Extra.thy		FSet_Extra.thy
Finite_Fun.thy		Finite_Fun.thy
Finite_Inj.thy		Finite_Inj.thy
Function_Toolkit.thy		Function_Toolkit.thy
Haskell_Show.thy		Haskell_Show.thy
Infinite_Sequence.thy		Infinite_Sequence.thy
Infinity.thy		Infinity.thy
List_Extra.thy		List_Extra.thy
Map_Extra.thy		Map_Extra.thy
Number_Toolkit.thy		Number_Toolkit.thy
Overriding.thy		Overriding.thy
Partial_Fun.thy		Partial_Fun.thy
Partial_Function_Command.ML		Partial_Function_Command.ML
Partial_Function_Command.thy		Partial_Function_Command.thy
Partial_Inj.thy		Partial_Inj.thy
Positive.thy		Positive.thy
README.md		README.md
ROOT		ROOT
Record_Default_Instance.ML		Record_Default_Instance.ML
Record_Default_Instance.thy		Record_Default_Instance.thy
Relation_Extra.thy		Relation_Extra.thy
Relation_Lib.thy		Relation_Lib.thy
Relation_Toolkit.thy		Relation_Toolkit.thy
Sequence_Toolkit.thy		Sequence_Toolkit.thy
Set_Toolkit.thy		Set_Toolkit.thy
Tabulate_Command.thy		Tabulate_Command.thy
Total_Fun.thy		Total_Fun.thy
Trace_Algebra.thy		Trace_Algebra.thy
Z_Toolkit.thy		Z_Toolkit.thy
Z_Toolkit_Overview.thy		Z_Toolkit_Overview.thy
Z_Toolkit_Pretty.thy		Z_Toolkit_Pretty.thy

Provide feedback