src/ZF/UNITY/Constrains.thy
changeset 24051 896fb015079c
parent 23894 1a4167d761ac
child 24893 b8ef7afe3a6b
     1.1 --- a/src/ZF/UNITY/Constrains.thy	Sun Jul 29 14:30:06 2007 +0200
     1.2 +++ b/src/ZF/UNITY/Constrains.thy	Sun Jul 29 14:30:07 2007 +0200
     1.3 @@ -533,7 +533,7 @@
     1.4  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
     1.5  
     1.6  (*To allow expansion of the program's definition when appropriate*)
     1.7 -val program_defs_ref = ref ([]: thm list);
     1.8 +structure ProgramDefs = NamedThmsFun(val name = "program" val description = "program definitions");
     1.9  
    1.10  (*proves "co" properties when the program is specified*)
    1.11  
    1.12 @@ -549,7 +549,7 @@
    1.13                (* Three subgoals *)
    1.14                rewrite_goal_tac [st_set_def] 3,
    1.15                REPEAT (force_tac css 2),
    1.16 -              full_simp_tac (ss addsimps !program_defs_ref) 1,
    1.17 +              full_simp_tac (ss addsimps (ProgramDefs.get ctxt)) 1,
    1.18                ALLGOALS (clarify_tac cs),
    1.19                REPEAT (FIRSTGOAL (etac disjE)),
    1.20                ALLGOALS (clarify_tac cs),
    1.21 @@ -564,6 +564,8 @@
    1.22      rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
    1.23  *}
    1.24  
    1.25 +setup ProgramDefs.setup
    1.26 +
    1.27  method_setup safety = {*
    1.28    Method.ctxt_args (fn ctxt =>
    1.29      Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}