# HG changeset patch
# User berghofe
# Date 908984882 -7200
# Node ID 0d28dbe484b6717a1fc33e90d8e807e6631432f9
# Parent  a3d2a6b6693e8199c670338b47ada126311f6b6f
Changed syntax of inductive.

diff -r a3d2a6b6693e -r 0d28dbe484b6 src/HOL/Induct/Acc.thy
--- a/src/HOL/Induct/Acc.thy	Wed Oct 21 17:46:00 1998 +0200
+++ b/src/HOL/Induct/Acc.thy	Wed Oct 21 17:48:02 1998 +0200
@@ -21,7 +21,7 @@
 inductive "acc(r)"
   intrs
     pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
-  monos     "[Pow_mono]"
+  monos     Pow_mono
 
 syntax        termi :: "('a * 'a)set => 'a set"
 translations "termi r" == "acc(r^-1)"
diff -r a3d2a6b6693e -r 0d28dbe484b6 src/HOL/Induct/Exp.thy
--- a/src/HOL/Induct/Exp.thy	Wed Oct 21 17:46:00 1998 +0200
+++ b/src/HOL/Induct/Exp.thy	Wed Oct 21 17:48:02 1998 +0200
@@ -27,7 +27,7 @@
     valOf  "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
             ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
 
-  monos "[exec_mono]"
+  monos exec_mono
 
 end
 
diff -r a3d2a6b6693e -r 0d28dbe484b6 src/HOL/Induct/Term.thy
--- a/src/HOL/Induct/Term.thy	Wed Oct 21 17:46:00 1998 +0200
+++ b/src/HOL/Induct/Term.thy	Wed Oct 21 17:48:02 1998 +0200
@@ -28,7 +28,7 @@
 inductive "term(A)"
   intrs
     APP_I "[| M: A;  N : list(term(A)) |] ==> Scons M N : term(A)"
-  monos   "[list_mono]"
+  monos   list_mono
 
 defs
   (*defining abstraction/representation functions for term list...*)
diff -r a3d2a6b6693e -r 0d28dbe484b6 src/HOL/Lambda/InductTermi.thy
--- a/src/HOL/Lambda/InductTermi.thy	Wed Oct 21 17:46:00 1998 +0200
+++ b/src/HOL/Lambda/InductTermi.thy	Wed Oct 21 17:48:02 1998 +0200
@@ -17,6 +17,6 @@
 VarI "rs : lists IT ==> (Var n)$$rs : IT"
 LambdaI "r : IT ==> Abs r : IT"
 BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
-monos "[lists_mono]"
+monos lists_mono
 
 end
diff -r a3d2a6b6693e -r 0d28dbe484b6 src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Wed Oct 21 17:46:00 1998 +0200
+++ b/src/HOL/ex/Primrec.thy	Wed Oct 21 17:48:02 1998 +0200
@@ -67,6 +67,6 @@
     PROJ     "PROJ i : PRIMREC"
     COMP     "[| g: PRIMREC; fs: lists PRIMREC |] ==> COMP g fs : PRIMREC"
     PREC     "[| f: PRIMREC; g: PRIMREC |] ==> PREC f g: PRIMREC"
-  monos      "[lists_mono]"
+  monos      lists_mono
 
 end