BETA_CONV `(\x. A) y` gives `|- (\x. A) y = A[y/x]` # BETA_CONV `(\x. x+2) 1` ;; val it : thm = |- (\x. x + 2) 1 = 1 + 2 AP_TERM `f` `ASM1 |- a = b` gives `ASM1 |- (f a) = (f b)` # AP_TERM `(\x. x+2)` (ASSUME`a=b:num`) ;; val it : thm = a …

今回からは，QUICK_REFERENCE.txt，VERYQUICK_REFERENCE.txtに沿って進みたいと思います．■ thm: (HOL Light's 10 primitive inference rules) + αREFL `x` gives `|- x = x` # REFL `x:num` ;; val it : thm = |- x = x # REFL `x:bool` ;; val it : thm = …