src/HOL/Hoare_Parallel/Hoare_Parallel.thy
author blanchet
Fri, 16 May 2014 12:56:39 +0200
changeset 56978 0c1b4987e6b2
parent 32621 a073cb249a06
permissions -rw-r--r--
proper handling of 'ctor_dtor' for mutual corecursive cases where not all type variables are present in all low-level constructors (cf. 'coind_wit1' etc. in 'Misc_Codatatypes.thy')

theory Hoare_Parallel
imports OG_Examples Gar_Coll Mul_Gar_Coll RG_Examples
begin

end