src/ZF/UNITY/Constrains.thy
changeset 31902 862ae16a799d
parent 30549 d2d7874648bd
child 32149 ef59550a55d3
     1.1 --- a/src/ZF/UNITY/Constrains.thy	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/ZF/UNITY/Constrains.thy	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -462,7 +462,11 @@
     1.4  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
     1.5  
     1.6  (*To allow expansion of the program's definition when appropriate*)
     1.7 -structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
     1.8 +structure Program_Defs = Named_Thms
     1.9 +(
    1.10 +  val name = "program"
    1.11 +  val description = "program definitions"
    1.12 +);
    1.13  
    1.14  (*proves "co" properties when the program is specified*)
    1.15  
    1.16 @@ -478,7 +482,7 @@
    1.17                (* Three subgoals *)
    1.18                rewrite_goal_tac [@{thm st_set_def}] 3,
    1.19                REPEAT (force_tac css 2),
    1.20 -              full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
    1.21 +              full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1,
    1.22                ALLGOALS (clarify_tac cs),
    1.23                REPEAT (FIRSTGOAL (etac disjE)),
    1.24                ALLGOALS (clarify_tac cs),
    1.25 @@ -493,7 +497,7 @@
    1.26      rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
    1.27  *}
    1.28  
    1.29 -setup ProgramDefs.setup
    1.30 +setup Program_Defs.setup
    1.31  
    1.32  method_setup safety = {*
    1.33    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}