--- a/NEWS Thu Aug 19 16:03:07 2010 +0200
+++ b/NEWS Thu Aug 19 16:08:53 2010 +0200
@@ -86,9 +86,18 @@
* Some previously unqualified names have been qualified:
types
+ bool ~> HOL.bool
nat ~> Nat.nat
constants
+ Trueprop ~> HOL.Trueprop
+ True ~> HOL.True
+ False ~> HOL.False
+ Not ~> HOL.Not
+ The ~> HOL.The
+ All ~> HOL.All
+ Ex ~> HOL.Ex
+ Ex1 ~> HOL.Ex1
Let ~> HOL.Let
If ~> HOL.If
Ball ~> Set.Ball
--- a/src/HOL/Import/HOL/bool.imp Thu Aug 19 16:03:07 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp Thu Aug 19 16:08:53 2010 +0200
@@ -12,11 +12,11 @@
"ARB" > "ARB_def"
const_maps
- "~" > "Not"
+ "~" > "HOL.Not"
"bool_case" > "Datatype.bool.bool_case"
"\\/" > "op |"
"TYPE_DEFINITION" > "HOL4Setup.TYPE_DEFINITION"
- "T" > "True"
+ "T" > "HOL.True"
"RES_SELECT" > "HOL4Base.bool.RES_SELECT"
"RES_FORALL" > "HOL4Base.bool.RES_FORALL"
"RES_EXISTS_UNIQUE" > "HOL4Base.bool.RES_EXISTS_UNIQUE"
@@ -25,13 +25,13 @@
"ONE_ONE" > "HOL4Setup.ONE_ONE"
"LET" > "HOL4Compat.LET"
"IN" > "HOL4Base.bool.IN"
- "F" > "False"
+ "F" > "HOL.False"
"COND" > "HOL.If"
"ARB" > "HOL4Base.bool.ARB"
- "?!" > "Ex1"
- "?" > "Ex"
+ "?!" > "HOL.Ex1"
+ "?" > "HOL.Ex"
"/\\" > "op &"
- "!" > "All"
+ "!" > "HOL.All"
thm_maps
"bool_case_thm" > "HOL4Base.bool.bool_case_thm"
--- a/src/HOL/Import/HOLLight/hollight.imp Thu Aug 19 16:03:07 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Thu Aug 19 16:08:53 2010 +0200
@@ -18,13 +18,13 @@
"finite_sum" > "HOLLight.hollight.finite_sum"
"finite_image" > "HOLLight.hollight.finite_image"
"cart" > "HOLLight.hollight.cart"
- "bool" > "bool"
+ "bool" > "HOL.bool"
"N_3" > "HOLLight.hollight.N_3"
"N_2" > "HOLLight.hollight.N_2"
"N_1" > "Product_Type.unit"
const_maps
- "~" > "Not"
+ "~" > "HOL.Not"
"two_2" > "HOLLight.hollight.two_2"
"two_1" > "HOLLight.hollight.two_1"
"treal_of_num" > "HOLLight.hollight.treal_of_num"
@@ -229,8 +229,8 @@
"ALL2" > "HOLLight.hollight.ALL2"
"ABS_prod" > "Abs_Prod"
"@" > "Hilbert_Choice.Eps"
- "?!" > "Ex1"
- "?" > "Ex"
+ "?!" > "HOL.Ex1"
+ "?" > "HOL.Ex"
">=" > "HOLLight.hollight.>="
">" > "HOLLight.hollight.>"
"==>" > "op -->"
@@ -243,7 +243,7 @@
"+" > "Groups.plus" :: "nat => nat => nat"
"*" > "Groups.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
- "!" > "All"
+ "!" > "HOL.All"
const_renames
"ALL" > "ALL_list"
--- a/src/HOL/Import/hol4rews.ML Thu Aug 19 16:03:07 2010 +0200
+++ b/src/HOL/Import/hol4rews.ML Thu Aug 19 16:08:53 2010 +0200
@@ -616,7 +616,7 @@
fun handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "=="}, _],_,_]] = x
| handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax all}, _],_]] = x
| handle_meta [x as Appl[Appl[Constant "_constrain", Constant @{const_syntax "==>"}, _],_,_]] = x
- | handle_meta [x] = Appl[Constant "Trueprop",x]
+ | handle_meta [x] = Appl[Constant @{const_syntax Trueprop}, x]
| handle_meta _ = error "hol4rews error: Trueprop not applied to single argument"
in
val smarter_trueprop_parsing = [(@{const_syntax Trueprop},handle_meta)]