User Tools

Site Tools


reference:attribute_examples

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
reference:attribute_examples [2011/07/07 12:09]
131.246.161.187 [where]
reference:attribute_examples [2011/07/25 12:32] (current)
131.246.41.159 [rotated]
Line 9: Line 9:
  
 Using Using
-    ​ 
     mp [of _ "C ∨ D"]     mp [of _ "C ∨ D"]
-    ​ 
 yields the more specific theorem yields the more specific theorem
  
Line 24: Line 22:
  
 Using Using
-  
     mp [where Q="C ∨ D"]     mp [where Q="C ∨ D"]
-  ​ 
 yields the more specific theorem yields the more specific theorem
  
Line 75: Line 71:
 Consider rule ''​disjE'':​ Consider rule ''​disjE'':​
  
-$\quad [|\ ?P \vee ?Q; ?P \Longrightarrow ?R; ?Q \Longrightarrow ?R\ |] \Longrightarrow ?R$.+$\quad [|\ ?P\;\vee\; ?Q; ?P \Longrightarrow ?R; ?Q \Longrightarrow ?R\ |] \Longrightarrow ?R$.
  
 Then,  Then, 
Line 82: Line 78:
 yields yields
  
-$\quad [\ ?Q \Longrightarrow ?R; ?P \vee ?Q; ?P \Longrightarrow ?R\ |] \Longrightarrow ?R$.+$\quad [|\ ?Q \Longrightarrow ?R; ?P\;\vee\; ?Q; ?P \Longrightarrow ?R\ |] \Longrightarrow ?R$.
 ==== symmetric ===== ==== symmetric =====
 Consider the definition of set membership ''​Set.mem_def'',​ Consider the definition of set membership ''​Set.mem_def'',​
reference/attribute_examples.1310033365.txt.gz · Last modified: 2011/07/07 12:09 by 131.246.161.187