# HG changeset patch
# User wenzelm
# Date 1188578793 -7200
# Node ID 5a3ee202e0b01d3246446112fc50dae6e9306d5b
# Parent  0a57b1b472b237591ab58e5bb085533032c02c4b
do not touch quick_and_dirty;

diff -r 0a57b1b472b2 -r 5a3ee202e0b0 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Fri Aug 31 16:17:53 2007 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Fri Aug 31 18:46:33 2007 +0200
@@ -12,7 +12,6 @@
 imports FOL
 begin
 
-ML {* set quick_and_dirty *}    (* allow for thm command in batch mode *)
 ML {* set Toplevel.debug *}
 ML {* set show_hyps *}
 ML {* set show_sorts *}
diff -r 0a57b1b472b2 -r 5a3ee202e0b0 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Fri Aug 31 16:17:53 2007 +0200
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Fri Aug 31 18:46:33 2007 +0200
@@ -8,6 +8,8 @@
 
 theory Pointer_Examples imports HeapSyntax begin
 
+axiomatization where unproven: "PROP A"
+
 section "Verifications"
 
 subsection "List reversal"
@@ -340,38 +342,35 @@
 consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool"
        path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list"
 
-ML"set quick_and_dirty"
-
 text"First some basic lemmas:"
 
 lemma [simp]: "ispath f p p"
-sorry
+by (rule unproven)
 lemma [simp]: "path f p p = []"
-sorry
+by (rule unproven)
 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q"
-sorry
+by (rule unproven)
 lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow>
  path (f(a := r)) p q = path f p q"
-sorry
+by (rule unproven)
 
 text"Some more specific lemmas needed by the example:"
 
 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q"
-sorry
+by (rule unproven)
 lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow>
  path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]"
-sorry
+by (rule unproven)
 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow>
  b \<notin> set (path f p (Ref a))"
-sorry
+by (rule unproven)
 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p"
-sorry
+by (rule unproven)
 lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]"
-sorry
+by (rule unproven)
 
 lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)"
-sorry
-ML"reset quick_and_dirty"
+by (rule unproven)
 
 lemma "VARS hd tl p q r s
  {islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and>