--- a/src/HOL/ex/Refute_Examples.thy Sun Jun 03 23:16:46 2007 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Sun Jun 03 23:16:47 2007 +0200
@@ -9,7 +9,6 @@
header {* Examples for the 'refute' command *}
theory Refute_Examples imports Main
-
begin
refute_params [satsolver="dpll"]
@@ -26,9 +25,9 @@
(******************************************************************************)
-section {* Examples and Test Cases *}
+subsection {* Examples and Test Cases *}
-subsection {* Propositional logic *}
+subsubsection {* Propositional logic *}
lemma "True"
refute
@@ -69,7 +68,7 @@
(******************************************************************************)
-subsection {* Predicate logic *}
+subsubsection {* Predicate logic *}
lemma "P x y z"
refute
@@ -85,7 +84,7 @@
(******************************************************************************)
-subsection {* Equality *}
+subsubsection {* Equality *}
lemma "P = True"
refute
@@ -119,7 +118,7 @@
(******************************************************************************)
-subsection {* First-Order Logic *}
+subsubsection {* First-Order Logic *}
lemma "\<exists>x. P x"
refute
@@ -213,7 +212,7 @@
(******************************************************************************)
-subsection {* Higher-Order Logic *}
+subsubsection {* Higher-Order Logic *}
lemma "\<exists>P. P"
refute
@@ -314,7 +313,7 @@
(******************************************************************************)
-subsection {* Meta-logic *}
+subsubsection {* Meta-logic *}
lemma "!!x. P x"
refute
@@ -346,7 +345,7 @@
(******************************************************************************)
-subsection {* Schematic variables *}
+subsubsection {* Schematic variables *}
lemma "?P"
refute
@@ -360,7 +359,7 @@
(******************************************************************************)
-subsection {* Abstractions *}
+subsubsection {* Abstractions *}
lemma "(\<lambda>x. x) = (\<lambda>x. y)"
refute
@@ -377,7 +376,7 @@
(******************************************************************************)
-subsection {* Sets *}
+subsubsection {* Sets *}
lemma "P (A::'a set)"
refute
@@ -422,7 +421,7 @@
(******************************************************************************)
-subsection {* arbitrary *}
+subsubsection {* arbitrary *}
lemma "arbitrary"
refute
@@ -442,7 +441,7 @@
(******************************************************************************)
-subsection {* The *}
+subsubsection {* The *}
lemma "The P"
refute
@@ -466,7 +465,7 @@
(******************************************************************************)
-subsection {* Eps *}
+subsubsection {* Eps *}
lemma "Eps P"
refute
@@ -491,7 +490,7 @@
(******************************************************************************)
-subsection {* Subtypes (typedef), typedecl *}
+subsubsection {* Subtypes (typedef), typedecl *}
text {* A completely unspecified non-empty subset of @{typ "'a"}: *}
@@ -513,7 +512,7 @@
(******************************************************************************)
-subsection {* Inductive datatypes *}
+subsubsection {* Inductive datatypes *}
text {* With @{text quick_and_dirty} set, the datatype package does
not generate certain axioms for recursion operators. Without these
@@ -521,7 +520,7 @@
ML {* reset quick_and_dirty *}
-subsubsection {* unit *}
+text {* unit *}
lemma "P (x::unit)"
refute
@@ -543,7 +542,7 @@
refute
oops
-subsubsection {* option *}
+text {* option *}
lemma "P (x::'a option)"
refute
@@ -569,7 +568,7 @@
refute
oops
-subsubsection {* * *}
+text {* * *}
lemma "P (x::'a*'b)"
refute
@@ -603,7 +602,7 @@
refute
oops
-subsubsection {* + *}
+text {* + *}
lemma "P (x::'a+'b)"
refute
@@ -633,7 +632,7 @@
refute
oops
-subsubsection {* Non-recursive datatypes *}
+text {* Non-recursive datatypes *}
datatype T1 = A | B
@@ -701,7 +700,7 @@
refute
oops
-subsubsection {* Recursive datatypes *}
+text {* Recursive datatypes *}
text {* nat *}
@@ -783,7 +782,7 @@
refute
oops
-subsubsection {* Mutually recursive datatypes *}
+text {* Mutually recursive datatypes *}
datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
and 'a bexp = Equal "'a aexp" "'a aexp"
@@ -824,7 +823,7 @@
refute
oops
-subsubsection {* Other datatype examples *}
+text {* Other datatype examples *}
datatype Trie = TR "Trie list"
@@ -915,7 +914,7 @@
(******************************************************************************)
-subsection {* Records *}
+subsubsection {* Records *}
(*TODO: make use of pair types, rather than typedef, for record types*)
@@ -936,7 +935,7 @@
(******************************************************************************)
-subsection {* Inductively defined sets *}
+subsubsection {* Inductively defined sets *}
consts
arbitrarySet :: "'a set"
@@ -974,7 +973,7 @@
(******************************************************************************)
-subsection {* Examples involving special functions *}
+subsubsection {* Examples involving special functions *}
lemma "card x = 0"
refute
@@ -1026,7 +1025,7 @@
(******************************************************************************)
-subsection {* Axiomatic type classes and overloading *}
+subsubsection {* Axiomatic type classes and overloading *}
text {* A type class without axioms: *}