Abstraction of enemy_analz_tac over its argument
authorpaulson
Fri Sep 13 18:48:25 1996 +0200 (1996-09-13)
changeset 2000adb88d42f1bd
parent 1999 b5efc4108d04
child 2001 974167c1d2c4
Abstraction of enemy_analz_tac over its argument
src/HOL/Auth/Shared.ML
     1.1 --- a/src/HOL/Auth/Shared.ML	Fri Sep 13 18:47:01 1996 +0200
     1.2 +++ b/src/HOL/Auth/Shared.ML	Fri Sep 13 18:48:25 1996 +0200
     1.3 @@ -12,6 +12,9 @@
     1.4  
     1.5  Addsimps [parts_cut_eq];
     1.6  
     1.7 +(*GOALS.ML??*)
     1.8 +fun prlim n = (goals_limit:=n; pr());
     1.9 +
    1.10  (*FUN.ML??  WE NEED A NOTION OF INVERSE IMAGE, OR GRAPH!!*)
    1.11  goal Set.thy "!!f. B <= range f = (B = f`` {x. f x: B})";
    1.12  by (fast_tac (!claset addEs [equalityE]) 1);
    1.13 @@ -224,8 +227,9 @@
    1.14      match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
    1.15      ORELSE' etac FalseE;
    1.16  
    1.17 -(*Analysis of Fake cases and of messages that forward unknown parts*)
    1.18 -val enemy_analz_tac =
    1.19 +(*Analysis of Fake cases and of messages that forward unknown parts
    1.20 +  Abstraction over i is ESSENTIAL: it delays the dereferencing of claset*)
    1.21 +fun enemy_analz_tac i =
    1.22    SELECT_GOAL 
    1.23     (EVERY [  (*push in occurrences of X...*)
    1.24  	   (REPEAT o CHANGED)
    1.25 @@ -238,6 +242,6 @@
    1.26  	   Fast_tac 1,
    1.27  	   Asm_full_simp_tac 1,
    1.28  	   IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1)
    1.29 -	   ]);
    1.30 +	   ]) i;
    1.31  
    1.32