(* * Copyright (C) 2014 NICTA * All rights reserved. *) (* Author: David Cock - David.Cock@nicta.com.au *) theory pGCL imports Algebra Automation Determinism Embedding Expectations Healthiness Induction LoopInduction Loops Misc StructuredReasoning Sublinearity Termination Transformers WellDefined begin end