src/HOL/Bali/AxExample.thy
changeset 17374 63e0ab9f2ea9
parent 16417 9bc16273c2d4
child 20195 ae79b9ad7224
equal deleted inserted replaced
17373:27509e72f29e 17374:63e0ab9f2ea9
    38 
    38 
    39 declare split_if_asm [split del]
    39 declare split_if_asm [split del]
    40 declare lvar_def [simp]
    40 declare lvar_def [simp]
    41 
    41 
    42 ML {*
    42 ML {*
    43 fun inst1_tac s t st = case assoc (rev (term_varnames (prop_of st)), s) of
    43 fun inst1_tac s t st = case AList.lookup (op =) (rev (term_varnames (prop_of st))) s of
    44   SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
    44   SOME i => Tactic.instantiate_tac' [((s, i), t)] st | NONE => Seq.empty;
    45 val ax_tac = REPEAT o rtac allI THEN'
    45 val ax_tac = REPEAT o rtac allI THEN'
    46              resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
    46              resolve_tac(thm "ax_Skip"::thm "ax_StatRef"::thm "ax_MethdN"::
    47                          thm "ax_Alloc"::thm "ax_Alloc_Arr"::
    47                          thm "ax_Alloc"::thm "ax_Alloc_Arr"::
    48                          thm "ax_SXAlloc_Normal"::
    48                          thm "ax_SXAlloc_Normal"::