src/FOLP/FOLP.thy
changeset 41779 a68f503805ed
parent 36319 8feb2c4bef1a
child 42799 4e33894aec6d
     1.1 --- a/src/FOLP/FOLP.thy	Fri Feb 18 16:36:42 2011 +0100
     1.2 +++ b/src/FOLP/FOLP.thy	Fri Feb 18 17:03:30 2011 +0100
     1.3 @@ -11,10 +11,8 @@
     1.4    ("classical.ML") ("simp.ML") ("simpdata.ML")
     1.5  begin
     1.6  
     1.7 -consts
     1.8 -  cla :: "[p=>p]=>p"
     1.9 -axioms
    1.10 -  classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    1.11 +axiomatization cla :: "[p=>p]=>p"
    1.12 +  where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
    1.13  
    1.14  
    1.15  (*** Classical introduction rules for | and EX ***)