modernized definitions;
authorwenzelm
Wed Oct 03 00:02:56 2007 +0200 (2007-10-03)
changeset 248197d8e0a47392e
parent 24818 d07e56a9a0c2
child 24820 c0c7e6ebf35f
modernized definitions;
src/HOL/ATP_Linkup.thy
     1.1 --- a/src/HOL/ATP_Linkup.thy	Tue Oct 02 22:23:31 2007 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Oct 03 00:02:56 2007 +0200
     1.3 @@ -23,33 +23,32 @@
     1.4    ("Tools/metis_tools.ML")
     1.5  begin
     1.6  
     1.7 -constdefs
     1.8 -  COMBI :: "'a => 'a"
     1.9 -    "COMBI P == P"
    1.10 +definition COMBI :: "'a => 'a"
    1.11 +  where "COMBI P == P"
    1.12 +
    1.13 +definition COMBK :: "'a => 'b => 'a"
    1.14 +  where "COMBK P Q == P"
    1.15  
    1.16 -  COMBK :: "'a => 'b => 'a"
    1.17 -    "COMBK P Q == P"
    1.18 +definition COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    1.19 +  where "COMBB P Q R == P (Q R)"
    1.20  
    1.21 -  COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c"
    1.22 -    "COMBB P Q R == P (Q R)"
    1.23 -
    1.24 -  COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    1.25 -    "COMBC P Q R == P R Q"
    1.26 +definition COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c"
    1.27 +  where "COMBC P Q R == P R Q"
    1.28  
    1.29 -  COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    1.30 -    "COMBS P Q R == P R (Q R)"
    1.31 +definition COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c"
    1.32 +  where "COMBS P Q R == P R (Q R)"
    1.33  
    1.34 -  COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
    1.35 -    "COMBB' M P Q R == M (P (Q R))"
    1.36 +definition COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c"
    1.37 +  where "COMBB' M P Q R == M (P (Q R))"
    1.38  
    1.39 -  COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
    1.40 -    "COMBC' M P Q R == M (P R) Q"
    1.41 +definition COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c"
    1.42 +  where "COMBC' M P Q R == M (P R) Q"
    1.43  
    1.44 -  COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
    1.45 -    "COMBS' M P Q R == M (P R) (Q R)"
    1.46 +definition COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c"
    1.47 +  where "COMBS' M P Q R == M (P R) (Q R)"
    1.48  
    1.49 -  fequal :: "'a => 'a => bool"
    1.50 -    "fequal X Y == (X=Y)"
    1.51 +definition fequal :: "'a => 'a => bool"
    1.52 +  where "fequal X Y == (X=Y)"
    1.53  
    1.54  lemma fequal_imp_equal: "fequal X Y ==> X=Y"
    1.55    by (simp add: fequal_def)