# HG changeset patch
# User blanchet
# Date 1267001994 -3600
# Node ID 38848da259c0027ac247f22526d5e74bb8170df6
# Parent  48e23510a3d896cd6537ca74cd6ded938592f505
got rid of "axclass", apparently

diff -r 48e23510a3d8 -r 38848da259c0 src/HOL/Nitpick_Examples/Refute_Nits.thy
--- a/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 09:19:21 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Refute_Nits.thy	Wed Feb 24 09:59:54 2010 +0100
@@ -1381,25 +1381,16 @@
 
 text {* A type class without axioms: *}
 
-axclass classA
+class classA
 
 lemma "P (x\<Colon>'a\<Colon>classA)"
 nitpick [expect = genuine]
 oops
 
-text {* The axiom of this type class does not contain any type variables: *}
-
-axclass classB
-classB_ax: "P \<or> \<not> P"
-
-lemma "P (x\<Colon>'a\<Colon>classB)"
-nitpick [expect = genuine]
-oops
-
 text {* An axiom with a type variable (denoting types which have at least two elements): *}
 
-axclass classC < type
-classC_ax: "\<exists>x y. x \<noteq> y"
+class classC =
+  assumes classC_ax: "\<exists>x y. x \<noteq> y"
 
 lemma "P (x\<Colon>'a\<Colon>classC)"
 nitpick [expect = genuine]
@@ -1411,11 +1402,9 @@
 
 text {* A type class for which a constant is defined: *}
 
-consts
-classD_const :: "'a \<Rightarrow> 'a"
-
-axclass classD < type
-classD_ax: "classD_const (classD_const x) = classD_const x"
+class classD =
+  fixes classD_const :: "'a \<Rightarrow> 'a"
+  assumes classD_ax: "classD_const (classD_const x) = classD_const x"
 
 lemma "P (x\<Colon>'a\<Colon>classD)"
 nitpick [expect = genuine]
@@ -1423,7 +1412,7 @@
 
 text {* A type class with multiple superclasses: *}
 
-axclass classE < classC, classD
+class classE = classC + classD
 
 lemma "P (x\<Colon>'a\<Colon>classE)"
 nitpick [expect = genuine]
diff -r 48e23510a3d8 -r 38848da259c0 src/HOL/Tools/Nitpick/HISTORY
--- a/src/HOL/Tools/Nitpick/HISTORY	Wed Feb 24 09:19:21 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY	Wed Feb 24 09:59:54 2010 +0100
@@ -2,6 +2,8 @@
 
   * Added and implemented "binary_ints" and "bits" options
   * Added "std" option and implemented support for nonstandard models
+  * Added support for local definitions
+  * Optimized "Multiset.multiset"
   * Fixed soundness bugs related to "destroy_constrs" optimization and record
     getters
   * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to