Event-B Theories - Revision history

Michael Leuschel: /* Download Theories */

2025-02-12T14:46:53Z

Download Theories

← Older revision		Revision as of 14:46, 12 February 2025
Line 10:		Line 10:
	== Download Theories ==		== Download Theories ==

	An example project with theories: [[media:theories2.zip]]		Here is an example Rodin project with several useful (standard) theories: [[media:theories2.zip]].

	The project contains the following theories:		The project contains the following theories:

2023-12-18T14:28:09Z

Error Messages

@@ Line 91: / Line 91: @@
   Axiomatic defined operator "SUM" not recognized.
 For reference, here are the contents of some of the <b>.ptm</b> files.
 In case of an error message, you can copy these files into your Theory Projects (e.g., using Drag & Drop) and then refresh (F5). After that animation with ProB should work.
@@ Line 105: / Line 106: @@
 <pre>
 operator "mk_iNAT" internal {mkinat}
 </pre>

2023-12-18T14:26:19Z

Tagging operators

@@ Line 69: / Line 69: @@
 It now also accepts many of its [[External_Functions|external functions]] as tag names, such as the
 the functions from LibraryStrings.def or LibraryReals.def.
 If you set the preference <tt> AUTO_DETECT_THEORY_MAPPING</tt> to TRUE then ProB will work with several standard Rodin theories even without a .ptm file in the workspace.

2022-09-27T16:24:35Z

Tagging operators

← Older revision		Revision as of 16:24, 27 September 2022
Line 69:		Line 69:
	It now also accepts many of its [[External_Functions\|external functions]] as tag names, such as the		It now also accepts many of its [[External_Functions\|external functions]] as tag names, such as the
	the functions from LibraryStrings.def or LibraryReals.def.		the functions from LibraryStrings.def or LibraryReals.def.
			If you set the preference <tt> AUTO_DETECT_THEORY_MAPPING</tt> to TRUE then ProB will work with several standard Rodin theories even without a .ptm file in the workspace.

2022-09-26T10:17:11Z

Tagging operators

← Older revision		Revision as of 10:17, 26 September 2022
Line 67:		Line 67:

	As of version 1.12 (mid-september 2022) ProB also transparently accepts <tt>POW(INT)</tt> as type for SIGMA and PI.		As of version 1.12 (mid-september 2022) ProB also transparently accepts <tt>POW(INT)</tt> as type for SIGMA and PI.
			It now also accepts many of its [[External_Functions\|external functions]] as tag names, such as the
			the functions from LibraryStrings.def or LibraryReals.def.

2022-09-21T12:13:20Z

Tagging operators

← Older revision		Revision as of 12:13, 21 September 2022
Line 55:		Line 55:
	\| closure1 \|\| the transitive closure \|\| POW(TT) \|\| POW(TT)		\| closure1 \|\| the transitive closure \|\| POW(TT) \|\| POW(TT)
	\|-		\|-
	\| SIGMA \|\| the sum of a set \|\| POW(T**INT) \|\| INT		\| SIGMA \|\| the sum of a set \|\| POW(T**INT) \|\| INT
	\|-		\|-
	\| PI \|\| the product of a set \|\| POW(T**INT) \|\| INT		\| PI \|\| the product of a set \|\| POW(T**INT) \|\| INT

2022-09-21T12:12:33Z

Tagging operators

← Older revision		Revision as of 12:12, 21 September 2022
Line 65:		Line 65:
	\| mkinat(zero,succ) \|\| returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) \|\| INT \|\| Inductive Nat		\| mkinat(zero,succ) \|\| returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) \|\| INT \|\| Inductive Nat
	\|}		\|}

			As of version 1.12 (mid-september 2022) ProB also transparently accepts <tt>POW(INT)</tt> as type for SIGMA and PI.

2015-10-13T10:05:54Z

Error Messages

@@ Line 72: / Line 72: @@
   Axiomatic defined operator "SUM" not recognized.
-For reference, here are some of the <b>.ptm</b> files:
+For reference, here are the contents of some of the <b>.ptm</b> files.
-*  [[media:SUMandPRODUCT.ptm]]
+In case of an error message, you can copy these files into your Theory Projects (e.g., using Drag & Drop) and then refresh (F5). After that animation with ProB should work.

2015-10-13T10:02:30Z

Error Messages

← Older revision		Revision as of 10:02, 13 October 2015
Line 73:		Line 73:

	For reference, here are some of the <b>.ptm</b> files:		For reference, here are some of the <b>.ptm</b> files:
	-		* [[media:SUMandPRODUCT.ptm]]

2015-10-13T10:01:54Z

Tagging operators

← Older revision		Revision as of 10:01, 13 October 2015
Line 65:		Line 65:
	\| mkinat(zero,succ) \|\| returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) \|\| INT \|\| Inductive Nat		\| mkinat(zero,succ) \|\| returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) \|\| INT \|\| Inductive Nat
	\|}		\|}


			=== Error Messages ===

			In case the <b>.ptm</b> file is missing, you will get an error message such as the following one:
			Axiomatic defined operator "SUM" not recognized.

			For reference, here are some of the <b>.ptm</b> files:
			-