src/HOL/Hoare_Parallel/Hoare_Parallel.thy
author wenzelm
Wed, 29 Jan 2025 20:17:21 +0100
changeset 82015 fe186fd7a168
parent 32621 a073cb249a06
permissions -rw-r--r--
make double sure that buffer.lineSeparator is well-defined: prevent a situation where $JEDIT_SETTINGS/properties would contain "buffer.lineSeparator=" and new-file would lead to a buffer with empty lineSeparator, and save would produce just one line;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 24104
diff changeset
     1
theory Hoare_Parallel
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 24104
diff changeset
     2
imports OG_Examples Gar_Coll Mul_Gar_Coll RG_Examples
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 24104
diff changeset
     3
begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     4
32621
a073cb249a06 theory entry point for session Hoare_Parallel (now also with proper underscore)
haftmann
parents: 24104
diff changeset
     5
end