# HG changeset patch
# User blanchet
# Date 1291638789 -3600
# Node ID 3eeb25d953d24e0ede321988f9b20d35b54bc009
# Parent  e538a4f9dd86fe6e89d7cce490a65c35670eab88
cleanup example

diff -r e538a4f9dd86 -r 3eeb25d953d2 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Mon Dec 06 13:33:09 2010 +0100
@@ -8,24 +8,9 @@
 header {* Examples Featuring Nitpick's Monotonicity Check *}
 
 theory Mono_Nits
-imports Nitpick2d(*###*) "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman"
+imports Main (* "~/afp/thys/AVL-Trees/AVL2" "~/afp/thys/Huffman/Huffman" *)
 begin
 
-(* ML {* Nitpick_Mono.first_calculus := false *} *)
-ML {* Nitpick_Mono.trace := true *}
-
-thm alphabet.simps
-
-fun alphabetx where
-"alphabetx (Leaf w a) = {a}" |
-"alphabetx (InnerNode w t\<^isub>1 t\<^isub>2) = alphabetx t\<^isub>1 \<union> alphabetx t\<^isub>2"
-
-lemma "\<exists>a. alphabetx (t::'a tree) (a::'a)"
-nitpick [debug, card = 1-2, dont_box, dont_finitize, dont_destroy_constrs]
-
-lemma "consistent t \<Longrightarrow> \<exists>a\<in>alphabet t. depth t a = Huffman.height t"
-nitpick [debug, card = 1-2, dont_box, dont_finitize]
-
 ML {*
 open Nitpick_Util
 open Nitpick_HOL
@@ -216,13 +201,15 @@
   in thy |> theorems_of |> List.app check_theorem end
 *}
 
-ML {* getenv "ISABELLE_TMP" *}
-
+(*
 ML {* check_theory @{theory AVL2} *}
 ML {* check_theory @{theory Fun} *}
 ML {* check_theory @{theory Huffman} *}
 ML {* check_theory @{theory List} *}
 ML {* check_theory @{theory Map} *}
 ML {* check_theory @{theory Relation} *}
+*)
+
+ML {* getenv "ISABELLE_TMP" *}
 
 end