src/HOL/TLA/Stfun.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6255 db63752140c7
child 12607 16b63730cfbb
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* 
     2     File:	 Stfun.ML
     3     Author:      Stephan Merz
     4     Copyright:   1998 University of Munich
     5 
     6 Lemmas and tactics for states and state functions.
     7 *)
     8 
     9 (*  [| basevars v; !!x. v x = c ==> Q |] ==> Q  *)
    10 bind_thm("baseE", (standard (basevars RS exE)));
    11 
    12 (* -------------------------------------------------------------------------------
    13    The following shows that there should not be duplicates in a "stvars" tuple:
    14 
    15 Goal "!!v. basevars (v::bool stfun, v) ==> False";
    16 by (etac baseE 1);
    17 by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1); 
    18 by (atac 2);
    19 by (Asm_full_simp_tac 1);
    20 
    21 ------------------------------------------------------------------------------- *)