# HG changeset patch
# User wenzelm
# Date 1330109231 -3600
# Node ID 61aac9bd43fab2d951c77a7edb15badb928e49f7
# Parent  5ba230f8232f0dffa128559150606ed8ad08125d# Parent  1258eab48270ae0afab29ac5ba097cdbf88780cc
merged

diff -r 5ba230f8232f -r 61aac9bd43fa Admin/isatest/isatest-stats
--- a/Admin/isatest/isatest-stats	Fri Feb 24 17:21:24 2012 +0100
+++ b/Admin/isatest/isatest-stats	Fri Feb 24 19:47:11 2012 +0100
@@ -52,6 +52,7 @@
   HOL-Proofs-Extraction
   HOL-Proofs-Lambda
   HOL-Proofs-ex
+  HOL-Quickcheck_Examples
   HOL-Quotient_Examples
   HOL-SET_Protocol
   HOL-SPARK
diff -r 5ba230f8232f -r 61aac9bd43fa src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Feb 24 17:21:24 2012 +0100
+++ b/src/HOL/IsaMakefile	Fri Feb 24 19:47:11 2012 +0100
@@ -1826,12 +1826,14 @@
 		$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz	\
 		$(LOG)/HOL-Lattice $(LOG)/HOL-Lattice.gz		\
 		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Library.gz			\
+		$(LOG)/HOL-Library-Codegenerator_Test.gz		\
 		$(LOG)/HOL-Main.gz $(LOG)/HOL-Matrix			\
 		$(LOG)/HOL-Matrix.gz $(LOG)/HOL-Metis_Examples.gz	\
 		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-Mirabelle.gz		\
 		$(LOG)/HOL-Multivariate_Analysis.gz			\
-		$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz		\
-		$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz	\
+		$(LOG)/HOL-Mutabelle.gz $(LOG)/HOL-NSA-Examples.gz	\
+		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NanoJava.gz		\
+		$(LOG)/HOL-Nitpick_Examples.gz				\
 		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz	\
 		$(LOG)/HOL-Number_Theory.gz				\
 		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
@@ -1839,19 +1841,22 @@
 		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
 		$(LOG)/HOL-Proofs.gz $(LOG)/HOL-Proofs-ex.gz		\
 		$(LOG)/HOL-Proofs-Extraction.gz				\
-		$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz	\
+		$(LOG)/HOL-Proofs-Lambda.gz				\
+		$(LOG)/HOL-Quickcheck_Examples.gz			\
+		$(LOG)/HOL-Quotient_Examples.gz				\
+		$(LOG)/HOL-SET_Protocol.gz				\
 		$(LOG)/HOL-Word-SMT_Examples.gz $(LOG)/HOL-SPARK.gz	\
 		$(LOG)/HOL-SPARK-Examples.gz				\
 		$(LOG)/HOL-SPARK-Manual.gz $(LOG)/HOL-Statespace.gz	\
-		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
-		$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz		\
-		$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz		\
-		$(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz $(LOG)/TLA-Inc.gz	\
-		$(LOG)/TLA-Memory.gz $(LOG)/TLA.gz $(OUT)/HOL		\
-		$(OUT)/HOL-Algebra $(OUT)/HOL-Base $(OUT)/HOL-Boogie	\
-		$(OUT)/HOL-IMP $(OUT)/HOL-Main				\
-		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
-		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain			\
+		$(LOG)/HOL-TPTP.gz $(LOG)/HOL-UNITY.gz			\
+		$(LOG)/HOL-Unix.gz $(LOG)/HOL-Word-Examples.gz		\
+		$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz	\
+		$(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz	\
+		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz	\
+		$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base		\
+		$(OUT)/HOL-Boogie $(OUT)/HOL-IMP $(OUT)/HOL-Library	\
+		$(OUT)/HOL-Main $(OUT)/HOL-Multivariate_Analysis	\
+		$(OUT)/HOL-NSA $(OUT)/HOL-Nominal $(OUT)/HOL-Plain	\
 		$(OUT)/HOL-Probability $(OUT)/HOL-Proofs		\
 		$(OUT)/HOL-SPARK $(OUT)/HOL-Word $(OUT)/HOL4		\
 		$(OUT)/TLA $(OUT)/HOLCF $(LOG)/HOLCF.gz			\
diff -r 5ba230f8232f -r 61aac9bd43fa src/Pure/PIDE/isabelle_markup.ML
--- a/src/Pure/PIDE/isabelle_markup.ML	Fri Feb 24 17:21:24 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Feb 24 19:47:11 2012 +0100
@@ -27,7 +27,7 @@
   val fbreakN: string val fbreak: Markup.T
   val hiddenN: string val hidden: Markup.T
   val classN: string
-  val typeN: string
+  val type_nameN: string
   val constantN: string
   val fixedN: string val fixed: string -> Markup.T
   val dynamic_factN: string val dynamic_fact: string -> Markup.T
@@ -174,7 +174,7 @@
 (* logical entities *)
 
 val classN = "class";
-val typeN = "type";
+val type_nameN = "type name";
 val constantN = "constant";
 
 val (fixedN, fixed) = markup_string "fixed" Markup.nameN;
diff -r 5ba230f8232f -r 61aac9bd43fa src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Fri Feb 24 17:21:24 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Feb 24 19:47:11 2012 +0100
@@ -78,7 +78,7 @@
   /* logical entities */
 
   val CLASS = "class"
-  val TYPE = "type"
+  val TYPE_NAME = "type name"
   val FIXED = "fixed"
   val CONSTANT = "constant"
 
diff -r 5ba230f8232f -r 61aac9bd43fa src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Feb 24 17:21:24 2012 +0100
+++ b/src/Pure/type.ML	Fri Feb 24 19:47:11 2012 +0100
@@ -187,7 +187,7 @@
 
 val empty_tsig =
   build_tsig ((Name_Space.empty Isabelle_Markup.classN, Sorts.empty_algebra), [],
-    Name_Space.empty_table Isabelle_Markup.typeN);
+    Name_Space.empty_table Isabelle_Markup.type_nameN);
 
 
 (* classes and sorts *)