15803

1 
(* Title: Pure/Pure.thy


2 
ID: $Id$


3 


4 
The Pure theory.


5 
*)


6 


7 
theory Pure


8 
imports ProtoPure


9 
begin


10 


11 
setup "Context.setup ()"


12 


13 

18019

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


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

15803

16 


17 
lemma meta_mp:

18019

18 
assumes "PROP P ==> PROP Q" and "PROP P"

15803

19 
shows "PROP Q"

18019

20 
by (rule `PROP P ==> PROP Q` [OF `PROP P`])

15803

21 


22 
lemma meta_spec:

18019

23 
assumes "!!x. PROP P(x)"

15803

24 
shows "PROP P(x)"

18019

25 
by (rule `!!x. PROP P(x)`)

15803

26 


27 
lemmas meta_allE = meta_spec [elim_format]


28 


29 
end
