# HG changeset patch
# User berghofe
# Date 899232675 -7200
# Node ID 8c782c25a11ecd942d5d3c117ca4ba9d1e56fb00
# Parent  52e7c75acfe64437884e2bb9a52f9d8112e57869
Adapted to new inductive definition package.

diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Auth/Message.ML	Tue Jun 30 20:51:15 1998 +0200
@@ -443,7 +443,7 @@
 \              analz (insert (Crypt K X) H) <= \
 \              insert (Crypt K X) (analz (insert X H))";
 by (rtac subsetI 1);
-by (eres_inst_tac [("za","x")] analz.induct 1);
+by (eres_inst_tac [("xa","x")] analz.induct 1);
 by (ALLGOALS (Blast_tac));
 val lemma1 = result();
 
@@ -451,7 +451,7 @@
 \              insert (Crypt K X) (analz (insert X H)) <= \
 \              analz (insert (Crypt K X) H)";
 by Auto_tac;
-by (eres_inst_tac [("za","x")] analz.induct 1);
+by (eres_inst_tac [("xa","x")] analz.induct 1);
 by Auto_tac;
 by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
 val lemma2 = result();
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
 Inductive relations "parts", "analz" and "synth"
 *)
 
-Message = Arith +
+Message = Arith + Inductive +
 
 (*Is there a difference between a nonce and arbitrary numerical data?
   Do we need a type of nonces?*)
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/IMP/Expr.thy
--- a/src/HOL/IMP/Expr.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/IMP/Expr.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
 Not used in the rest of the language, but included for completeness.
 *)
 
-Expr = Arith +
+Expr = Arith + Inductive +
 
 (** Arithmetic expressions **)
 types loc
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/IMP/Hoare.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -6,7 +6,7 @@
 Inductive definition of Hoare logic
 *)
 
-Hoare = Denotation + Gfp +
+Hoare = Denotation + Inductive +
 
 types assn = state => bool
 
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/IMP/Natural.thy
--- a/src/HOL/IMP/Natural.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/IMP/Natural.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -6,7 +6,7 @@
 Natural semantics of commands
 *)
 
-Natural = Com +
+Natural = Com + Inductive +
 
 (** Execution of commands **)
 consts  evalc    :: "(com*state*state)set"
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Induct/Acc.thy
--- a/src/HOL/Induct/Acc.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Induct/Acc.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -9,7 +9,7 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-Acc = WF + 
+Acc = WF + Inductive +
 
 constdefs
   pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Induct/Com.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -6,7 +6,7 @@
 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
 *)
 
-Com = Arith +
+Com = Arith + Inductive +
 
 types loc
       state = "loc => nat"
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Induct/Comb.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -13,7 +13,7 @@
 *)
 
 
-Comb = Arith +
+Comb = Arith + Inductive +
 
 (** Datatype definition of combinators S and K, with infixed application **)
 datatype comb = K
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Induct/LList.ML	Tue Jun 30 20:51:15 1998 +0200
@@ -544,8 +544,8 @@
     [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
 by (Fast_tac 1);
 by Safe_tac;
-by (eres_inst_tac [("a", "u")] llist.elim 1);
-by (eres_inst_tac [("a", "v")] llist.elim 1);
+by (eres_inst_tac [("aa", "u")] llist.elim 1);
+by (eres_inst_tac [("aa", "v")] llist.elim 1);
 by (ALLGOALS Asm_simp_tac);
 by (Blast_tac 1);
 qed "Lappend_type";
@@ -556,7 +556,7 @@
 by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
 by (etac imageI 1);
 by (rtac image_subsetI 1);
-by (eres_inst_tac [("a", "x")] llist.elim 1);
+by (eres_inst_tac [("aa", "x")] llist.elim 1);
 by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
 by (Asm_simp_tac 1);
 qed "Lappend_type";
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Inductive.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -1,3 +1,4 @@
-Inductive = Gfp + Prod + Sum + "indrule"
+Inductive = Gfp + Prod + Sum +
 
+end
 
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
 substitution and beta-reduction.
 *)
 
-Lambda = Arith +
+Lambda = Arith + Inductive +
 
 datatype dB = Var nat | "@" dB dB (infixl 200) | Abs dB
 
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOL/ex/MT.thy
--- a/src/HOL/ex/MT.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/ex/MT.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -13,7 +13,7 @@
     Report 308, Computer Lab, University of Cambridge (1993).
 *)
 
-MT = Gfp + Sum + 
+MT = Inductive + 
 
 types 
   Const
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Jun 30 20:51:15 1998 +0200
@@ -242,7 +242,7 @@
 \  ==> invariant A P";
 by (rtac allI 1);
 by (rtac impI 1);
-by (res_inst_tac [("za","s")] reachable.induct 1);
+by (res_inst_tac [("xa","s")] reachable.induct 1);
 by (atac 1);
 by (etac p1 1);
 by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1);
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
 *)   
 
 		       
-Automata = Option + Asig +  
+Automata = Option + Asig + Inductive +
 
 default term
  
diff -r 52e7c75acfe6 -r 8c782c25a11e src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Tue Jun 30 20:51:15 1998 +0200
@@ -7,7 +7,7 @@
 *)  
 
 
-Seq = HOLCF + 
+Seq = HOLCF + Inductive +
 
 domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq)  (infixr 65)