src/HOL/UNITY/Extend.ML
1999-10-11 paulson 1999-10-11 working shapshot with "projecting" and "extending"
1999-10-04 paulson 1999-10-04 working snapshot (even Alloc)
1999-09-30 paulson 1999-09-30 now with (weak safety) guarantees (weak progress) with Extend
1999-09-29 paulson 1999-09-29 working snapshot with new theory "Project"
1999-09-24 paulson 1999-09-24 working version with co-guarantees-leadsto results
1999-09-21 paulson 1999-09-21 project_act no longer has a special case to allow identity actions
1999-09-17 paulson 1999-09-17 new rule PLam_ensures
1999-09-10 paulson 1999-09-10 working snapshot
1999-09-07 wenzelm 1999-09-07 isatool expandshort;
1999-09-06 paulson 1999-09-06 working snapshot
1999-08-31 paulson 1999-08-31 changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
1999-08-30 paulson 1999-08-30 new results for localTo
1999-08-27 paulson 1999-08-27 use of bij, new theorems, etc.
1999-08-26 paulson 1999-08-26 new laws; changed "guar" back to "guarantees" (sorry)
1999-08-25 paulson 1999-08-25 many "project" laws
1999-06-17 paulson 1999-06-17 renamed UNION_... to UN_..., INTER_... to INT_... (to fit the convention)
1999-06-13 paulson 1999-06-13 guarantees -> guar
1999-05-17 paulson 1999-05-17 new thm extend_JN; renamed extend_leadsto
1999-04-29 paulson 1999-04-29 made many specification operators infix
1999-04-20 paulson 1999-04-20 new result extend_LeadsTo
1999-03-09 paulson 1999-03-09 tidied
1999-03-03 paulson 1999-03-03 new theory of extending the state space