# HG changeset patch
# User berghofe
# Date 1028731808 -7200
# Node ID aed3aef2a0ca94defbfc6c49b1d82382a156b28c
# Parent  d2cbbad84ad334e3e6cc4736bc3e3b01aa1b3cbc
Removed (now unneeded) declaration of realizer for induction on datatype b.

diff -r d2cbbad84ad3 -r aed3aef2a0ca src/HOL/Extraction/Warshall.thy
--- a/src/HOL/Extraction/Warshall.thy	Wed Aug 07 16:49:25 2002 +0200
+++ b/src/HOL/Extraction/Warshall.thy	Wed Aug 07 16:50:08 2002 +0200
@@ -14,14 +14,6 @@
 
 datatype b = T | F
 
-theorem b_ind_realizer:
-  "R x T \<Longrightarrow> R y F \<Longrightarrow> R (case b of T \<Rightarrow> x | F \<Rightarrow> y) b"
-  by (induct b, simp_all)
-
-realizers
-  b.induct (P): "\<lambda>P b x y. (case b of T \<Rightarrow> x | F \<Rightarrow> y)"
-    "\<Lambda>P b x (h: _) y. b_ind_realizer \<cdot> (\<lambda>x b. realizes x (P b)) \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> h"
-
 consts
   is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"