src/HOL/UNITY/Rename.thy
changeset 13798 4c1a53627500
parent 13790 8d7e9fce8c50
child 13805 3786b2fd6808
     1.1 --- a/src/HOL/UNITY/Rename.thy	Thu Jan 30 18:08:09 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Rename.thy	Fri Jan 31 20:12:44 2003 +0100
     1.3 @@ -2,9 +2,9 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   2000  University of Cambridge
     1.7 +*)
     1.8  
     1.9 -Renaming of state sets
    1.10 -*)
    1.11 +header{*Renaming of State Sets*}
    1.12  
    1.13  theory Rename = Extend:
    1.14  
    1.15 @@ -42,7 +42,7 @@
    1.16  by (simp add: rename_def)
    1.17  
    1.18  
    1.19 -(*** inverse properties ***)
    1.20 +subsection{*inverse properties*}
    1.21  
    1.22  lemma extend_set_inv: 
    1.23       "bij h  
    1.24 @@ -166,7 +166,7 @@
    1.25  by (blast intro: bij_rename bij_rename_imp_bij)
    1.26  
    1.27  
    1.28 -(*** the lattice operations ***)
    1.29 +subsection{*the lattice operations*}
    1.30  
    1.31  lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
    1.32  by (simp add: rename_def Extend.extend_SKIP)
    1.33 @@ -180,7 +180,7 @@
    1.34  by (simp add: rename_def Extend.extend_JN)
    1.35  
    1.36  
    1.37 -(*** Strong Safety: co, stable ***)
    1.38 +subsection{*Strong Safety: co, stable*}
    1.39  
    1.40  lemma rename_constrains: 
    1.41       "bij h ==> (rename h F : (h`A) co (h`B)) = (F : A co B)"
    1.42 @@ -205,7 +205,7 @@
    1.43  done
    1.44  
    1.45  
    1.46 -(*** Weak Safety: Co, Stable ***)
    1.47 +subsection{*Weak Safety: Co, Stable*}
    1.48  
    1.49  lemma reachable_rename_eq: 
    1.50       "bij h ==> reachable (rename h F) = h ` (reachable F)"
    1.51 @@ -230,7 +230,7 @@
    1.52                bij_is_surj [THEN surj_f_inv_f])
    1.53  
    1.54  
    1.55 -(*** Progress: transient, ensures ***)
    1.56 +subsection{*Progress: transient, ensures*}
    1.57  
    1.58  lemma rename_transient: 
    1.59       "bij h ==> (rename h F : transient (h`A)) = (F : transient A)"
    1.60 @@ -290,7 +290,7 @@
    1.61  by (simp add: Extend.OK_extend_iff rename_def)
    1.62  
    1.63  
    1.64 -(*** "image" versions of the rules, for lifting "guarantees" properties ***)
    1.65 +subsection{*"image" versions of the rules, for lifting "guarantees" properties*}
    1.66  
    1.67  (*All the proofs are similar.  Better would have been to prove one 
    1.68    meta-theorem, but how can we handle the polymorphism?  E.g. in