tuned ML code;
authorwenzelm
Tue Jul 25 21:18:01 2006 +0200 (2006-07-25)
changeset 20195ae79b9ad7224
parent 20194 c9dbce9a23a1
child 20196 9a19e4de6e2e
tuned ML code;
src/HOL/Bali/AxExample.thy
     1.1 --- a/src/HOL/Bali/AxExample.thy	Tue Jul 25 21:18:00 2006 +0200
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Tue Jul 25 21:18:01 2006 +0200
     1.3 @@ -40,13 +40,25 @@
     1.4  declare lvar_def [simp]
     1.5  
     1.6  ML {*
     1.7 -fun inst1_tac s t st = case AList.lookup (op =) (rev (term_varnames (prop_of st))) s of
     1.8 +local
     1.9 +  val ax_Skip = thm "ax_Skip";
    1.10 +  val ax_StatRef = thm "ax_StatRef";
    1.11 +  val ax_MethdN = thm "ax_MethdN";
    1.12 +  val ax_Alloc = thm "ax_Alloc";
    1.13 +  val ax_Alloc_Arr = thm "ax_Alloc_Arr";
    1.14 +  val ax_SXAlloc_Normal = thm "ax_SXAlloc_Normal";
    1.15 +  val ax_derivs_intros = funpow 7 tl (thms "ax_derivs.intros");
    1.16 +in
    1.17 +
    1.18 +fun inst1_tac s t st =
    1.19 +  case AList.lookup (op =) (rev (Term.add_varnames (prop_of st) [])) s of
    1.20    SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
    1.21 -val ax_tac = REPEAT o rtac allI THEN'
    1.22 -             resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
    1.23 -                         thm "ax_Alloc"::thm "ax_Alloc_Arr"::
    1.24 -                         thm "ax_SXAlloc_Normal"::
    1.25 -                         funpow 7 tl (thms "ax_derivs.intros"))
    1.26 +
    1.27 +val ax_tac =
    1.28 +  REPEAT o rtac allI THEN'
    1.29 +  resolve_tac (ax_Skip :: ax_StatRef :: ax_MethdN :: ax_Alloc ::
    1.30 +    ax_Alloc_Arr :: ax_SXAlloc_Normal :: ax_derivs_intros);
    1.31 +end;
    1.32  *}
    1.33  
    1.34