deglobalized named HOL constants
authorhaftmann
Thu Aug 19 16:08:53 2010 +0200 (2010-08-19)
changeset 38556dc92eee56ed7
parent 38555 bd6359ed1636
child 38557 9926c47ad1a1
deglobalized named HOL constants
NEWS
src/HOL/Import/HOL/bool.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Import/hol4rews.ML
     1.1 --- a/NEWS	Thu Aug 19 16:03:07 2010 +0200
     1.2 +++ b/NEWS	Thu Aug 19 16:08:53 2010 +0200
     1.3 @@ -86,9 +86,18 @@
     1.4  * Some previously unqualified names have been qualified:
     1.5  
     1.6    types
     1.7 +    bool ~> HOL.bool
     1.8      nat ~> Nat.nat
     1.9  
    1.10    constants
    1.11 +    Trueprop ~> HOL.Trueprop
    1.12 +    True ~> HOL.True
    1.13 +    False ~> HOL.False
    1.14 +    Not ~> HOL.Not
    1.15 +    The ~> HOL.The
    1.16 +    All ~> HOL.All
    1.17 +    Ex ~> HOL.Ex
    1.18 +    Ex1 ~> HOL.Ex1
    1.19      Let ~> HOL.Let
    1.20      If ~> HOL.If
    1.21      Ball ~> Set.Ball
     2.1 --- a/src/HOL/Import/HOL/bool.imp	Thu Aug 19 16:03:07 2010 +0200
     2.2 +++ b/src/HOL/Import/HOL/bool.imp	Thu Aug 19 16:08:53 2010 +0200
     2.3 @@ -12,11 +12,11 @@
     2.4    "ARB" > "ARB_def"
     2.5  
     2.6  const_maps
     2.7 -  "~" > "Not"
     2.8 +  "~" > "HOL.Not"
     2.9    "bool_case" > "Datatype.bool.bool_case"
    2.10    "\\/" > "op |"
    2.11    "TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
    2.12 -  "T" > "True"
    2.13 +  "T" > "HOL.True"
    2.14    "RES_SELECT" > "HOL4Base.bool.RES_SELECT"
    2.15    "RES_FORALL" > "HOL4Base.bool.RES_FORALL"
    2.16    "RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
    2.17 @@ -25,13 +25,13 @@
    2.18    "ONE_ONE" > "HOL4Setup.ONE_ONE"
    2.19    "LET" > "HOL4Compat.LET"
    2.20    "IN" > "HOL4Base.bool.IN"
    2.21 -  "F" > "False"
    2.22 +  "F" > "HOL.False"
    2.23    "COND" > "HOL.If"
    2.24    "ARB" > "HOL4Base.bool.ARB"
    2.25 -  "?!" > "Ex1"
    2.26 -  "?" > "Ex"
    2.27 +  "?!" > "HOL.Ex1"
    2.28 +  "?" > "HOL.Ex"
    2.29    "/\\" > "op &"
    2.30 -  "!" > "All"
    2.31 +  "!" > "HOL.All"
    2.32  
    2.33  thm_maps
    2.34    "bool_case_thm" > "HOL4Base.bool.bool_case_thm"
     3.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 19 16:03:07 2010 +0200
     3.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Aug 19 16:08:53 2010 +0200
     3.3 @@ -18,13 +18,13 @@
     3.4    "finite_sum" > "HOLLight.hollight.finite_sum"
     3.5    "finite_image" > "HOLLight.hollight.finite_image"
     3.6    "cart" > "HOLLight.hollight.cart"
     3.7 -  "bool" > "bool"
     3.8 +  "bool" > "HOL.bool"
     3.9    "N_3" > "HOLLight.hollight.N_3"
    3.10    "N_2" > "HOLLight.hollight.N_2"
    3.11    "N_1" > "Product_Type.unit"
    3.12  
    3.13  const_maps
    3.14 -  "~" > "Not"
    3.15 +  "~" > "HOL.Not"
    3.16    "two_2" > "HOLLight.hollight.two_2"
    3.17    "two_1" > "HOLLight.hollight.two_1"
    3.18    "treal_of_num" > "HOLLight.hollight.treal_of_num"
    3.19 @@ -229,8 +229,8 @@
    3.20    "ALL2" > "HOLLight.hollight.ALL2"
    3.21    "ABS_prod" > "Abs_Prod"
    3.22    "@" > "Hilbert_Choice.Eps"
    3.23 -  "?!" > "Ex1"
    3.24 -  "?" > "Ex"
    3.25 +  "?!" > "HOL.Ex1"
    3.26 +  "?" > "HOL.Ex"
    3.27    ">=" > "HOLLight.hollight.>="
    3.28    ">" > "HOLLight.hollight.>"
    3.29    "==>" > "op -->"
    3.30 @@ -243,7 +243,7 @@
    3.31    "+" > "Groups.plus" :: "nat => nat => nat"
    3.32    "*" > "Groups.times" :: "nat => nat => nat"
    3.33    "$" > "HOLLight.hollight.$"
    3.34 -  "!" > "All"
    3.35 +  "!" > "HOL.All"
    3.36  
    3.37  const_renames
    3.38    "ALL" > "ALL_list"
     4.1 --- a/src/HOL/Import/hol4rews.ML	Thu Aug 19 16:03:07 2010 +0200
     4.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Aug 19 16:08:53 2010 +0200
     4.3 @@ -616,7 +616,7 @@
     4.4      fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
     4.5        | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
     4.6        | handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
     4.7 -      | handle_meta [x] = Appl[Constant "Trueprop",x]
     4.8 +      | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
     4.9        | handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
    4.10  in
    4.11  val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]