src/HOL/TLA/Intensional.thy
changeset 35108 e384e27c229f
parent 31945 d5f186aa0bed
child 35318 e1b61c5fd494
     1.1 --- a/src/HOL/TLA/Intensional.thy	Thu Feb 11 13:54:53 2010 +0100
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Thu Feb 11 21:31:50 2010 +0100
     1.3 @@ -1,8 +1,6 @@
     1.4 -(*
     1.5 -    File:        TLA/Intensional.thy
     1.6 -    ID:          $Id$
     1.7 -    Author:      Stephan Merz
     1.8 -    Copyright:   1998 University of Munich
     1.9 +(*  Title:      HOL/TLA/Intensional.thy
    1.10 +    Author:     Stephan Merz
    1.11 +    Copyright:  1998 University of Munich
    1.12  *)
    1.13  
    1.14  header {* A framework for "intensional" (possible-world based) logics
    1.15 @@ -95,11 +93,11 @@
    1.16    "_REx1" :: "[idts, lift] => lift"                      ("(3EX! _./ _)" [0, 10] 10)
    1.17  
    1.18  translations
    1.19 -  "_const"        == "const"
    1.20 -  "_lift"         == "lift"
    1.21 -  "_lift2"        == "lift2"
    1.22 -  "_lift3"        == "lift3"
    1.23 -  "_Valid"        == "Valid"
    1.24 +  "_const"        == "CONST const"
    1.25 +  "_lift"         == "CONST lift"
    1.26 +  "_lift2"        == "CONST lift2"
    1.27 +  "_lift3"        == "CONST lift3"
    1.28 +  "_Valid"        == "CONST Valid"
    1.29    "_RAll x A"     == "Rall x. A"
    1.30    "_REx x  A"     == "Rex x. A"
    1.31    "_REx1 x  A"    == "Rex! x. A"
    1.32 @@ -112,11 +110,11 @@
    1.33  
    1.34    "_liftEqu"      == "_lift2 (op =)"
    1.35    "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
    1.36 -  "_liftNot"      == "_lift Not"
    1.37 +  "_liftNot"      == "_lift (CONST Not)"
    1.38    "_liftAnd"      == "_lift2 (op &)"
    1.39    "_liftOr"       == "_lift2 (op | )"
    1.40    "_liftImp"      == "_lift2 (op -->)"
    1.41 -  "_liftIf"       == "_lift3 If"
    1.42 +  "_liftIf"       == "_lift3 (CONST If)"
    1.43    "_liftPlus"     == "_lift2 (op +)"
    1.44    "_liftMinus"    == "_lift2 (op -)"
    1.45    "_liftTimes"    == "_lift2 (op *)"
    1.46 @@ -126,12 +124,12 @@
    1.47    "_liftLeq"      == "_lift2 (op <=)"
    1.48    "_liftMem"      == "_lift2 (op :)"
    1.49    "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
    1.50 -  "_liftFinset (_liftargs x xs)"  == "_lift2 CONST insert x (_liftFinset xs)"
    1.51 -  "_liftFinset x" == "_lift2 CONST insert x (_const {})"
    1.52 +  "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
    1.53 +  "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
    1.54    "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
    1.55 -  "_liftPair"     == "_lift2 Pair"
    1.56 -  "_liftCons"     == "lift2 Cons"
    1.57 -  "_liftApp"      == "lift2 (op @)"
    1.58 +  "_liftPair"     == "_lift2 (CONST Pair)"
    1.59 +  "_liftCons"     == "CONST lift2 (CONST Cons)"
    1.60 +  "_liftApp"      == "CONST lift2 (op @)"
    1.61    "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
    1.62    "_liftList x"   == "_liftCons x (_const [])"
    1.63