--- a/src/HOL/UNITY/SubstAx.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Mon Mar 01 13:40:23 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/UNITY/SubstAx
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1998 University of Cambridge
@@ -10,11 +9,10 @@
theory SubstAx imports WFair Constrains begin
-constdefs
- Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60)
+definition Ensures :: "['a set, 'a set] => 'a program set" (infixl "Ensures" 60) where
"A Ensures B == {F. F \<in> (reachable F \<inter> A) ensures B}"
- LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60)
+definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where
"A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
syntax (xsymbols)