prefer vacuous definitional type classes over axiomatic ones;
authorwenzelm
Mon Feb 10 21:00:56 2014 +0100 (2014-02-10)
changeset 553829218fa411c15
parent 55381 ca31f042414f
child 55383 a416780523e2
prefer vacuous definitional type classes over axiomatic ones;
src/HOL/TLA/Action.thy
src/HOL/TLA/Init.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Stfun.thy
     1.1 --- a/src/HOL/TLA/Action.thy	Mon Feb 10 17:23:13 2014 +0100
     1.2 +++ b/src/HOL/TLA/Action.thy	Mon Feb 10 21:00:56 2014 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4  type_synonym 'a trfun = "(state * state) => 'a"
     1.5  type_synonym action   = "bool trfun"
     1.6  
     1.7 -arities prod :: (world, world) world
     1.8 +instance prod :: (world, world) world ..
     1.9  
    1.10  consts
    1.11    (** abstract syntax **)
     2.1 --- a/src/HOL/TLA/Init.thy	Mon Feb 10 17:23:13 2014 +0100
     2.2 +++ b/src/HOL/TLA/Init.thy	Mon Feb 10 21:00:56 2014 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4  begin
     2.5  
     2.6  typedecl behavior
     2.7 -arities behavior :: world
     2.8 +instance behavior :: world ..
     2.9  
    2.10  type_synonym temporal = "behavior form"
    2.11  
     3.1 --- a/src/HOL/TLA/Intensional.thy	Mon Feb 10 17:23:13 2014 +0100
     3.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Feb 10 21:00:56 2014 +0100
     3.3 @@ -10,8 +10,7 @@
     3.4  imports Main
     3.5  begin
     3.6  
     3.7 -classes world
     3.8 -classrel world < type
     3.9 +class world
    3.10  
    3.11  (** abstract syntax **)
    3.12  
     4.1 --- a/src/HOL/TLA/Stfun.thy	Mon Feb 10 17:23:13 2014 +0100
     4.2 +++ b/src/HOL/TLA/Stfun.thy	Mon Feb 10 21:00:56 2014 +0100
     4.3 @@ -10,8 +10,7 @@
     4.4  begin
     4.5  
     4.6  typedecl state
     4.7 -
     4.8 -arities state :: world
     4.9 +instance state :: world ..
    4.10  
    4.11  type_synonym 'a stfun = "state => 'a"
    4.12  type_synonym stpred  = "bool stfun"