| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/TLA/Memory/ (Beweissystem Isabelle Version 2025-1©) Datei vom 16.11.2025 mit Größe 576 B |
|
Quelle RPCMemoryParams.thy Sprache: Isabelle |
|||||||||
|
(* Title: HOL/TLA/Memory/RPCMemoryParams.thy
Author: Stephan Merz, University of Munich *) section \<open>Basic declarations for the RPC-memory example\<close> theory RPCMemoryParams imports Main begin type_synonym bit = "bool" (* Signal wires for the procedure interface. Defined as bool for simplicity. All I should really need is the existence of two distinct values. *) (* all of these are simple (HOL) types *) typedecl Locs (* "syntactic" value type *) typedecl Vals (* "syntactic" value type *) typedecl PrIds (* process id's *) end ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28