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