src/HOL/TLA/Intensional.thy
changeset 24180 9f818139951b
parent 21624 6f79647cf536
child 30528 7173bf123335
     1.1 --- a/src/HOL/TLA/Intensional.thy	Tue Aug 07 20:43:36 2007 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Tue Aug 07 23:24:10 2007 +0200
     1.3 @@ -243,24 +243,17 @@
     1.4  (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
     1.5  
     1.6  ML {*
     1.7 -
     1.8 -local
     1.9 -  val intD = thm "intD";
    1.10 -  val inteq_reflection = thm "inteq_reflection";
    1.11 -  val intensional_rews = thms "intensional_rews";
    1.12 -in
    1.13 -
    1.14  (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
    1.15     |- F = G    becomes   F w = G w
    1.16     |- F --> G  becomes   F w --> G w
    1.17  *)
    1.18  
    1.19  fun int_unlift th =
    1.20 -  rewrite_rule intensional_rews (th RS intD handle THM _ => th);
    1.21 +  rewrite_rule @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);
    1.22  
    1.23  (* Turn  |- F = G  into meta-level rewrite rule  F == G *)
    1.24  fun int_rewrite th =
    1.25 -  zero_var_indexes (rewrite_rule intensional_rews (th RS inteq_reflection))
    1.26 +  zero_var_indexes (rewrite_rule @{thms intensional_rews} (th RS @{thm inteq_reflection}))
    1.27  
    1.28  (* flattening turns "-->" into "==>" and eliminates conjunctions in the
    1.29     antecedent. For example,
    1.30 @@ -299,8 +292,6 @@
    1.31        Const _ $ (Const ("Intensional.Valid", _) $ _) =>
    1.32                (flatten (int_unlift th) handle THM _ => th)
    1.33      | _ => th
    1.34 -
    1.35 -end
    1.36  *}
    1.37  
    1.38  setup {*