15803

1 
(* Title: Pure/Pure.thy


2 
ID: $Id$


3 
Author: Larry Paulson and Makarius


4 


5 
The Pure theory.


6 
*)


7 


8 
theory Pure


9 
imports ProtoPure


10 
begin


11 


12 
setup "Context.setup ()"


13 


14 


15 
text{*These metalevel elimination rules facilitate the use of assumptions


16 
that contain !! and ==>, especially in linear scripts. *}


17 


18 
lemma meta_mp:


19 
assumes major: "PROP P ==> PROP Q" and minor: "PROP P"


20 
shows "PROP Q"


21 
proof 


22 
show "PROP Q" by (rule major [OF minor])


23 
qed


24 


25 
lemma meta_spec:


26 
assumes major: "!!x. PROP P(x)"


27 
shows "PROP P(x)"


28 
proof 


29 
show "PROP P(x)" by (rule major)


30 
qed


31 


32 
lemmas meta_allE = meta_spec [elim_format]


33 


34 
end
