# HG changeset patch
# User wenzelm
# Date 961603749 -7200
# Node ID b643f4d7b9e97d621cdfdd2c0ac28c65ddd12de9
# Parent  9e081c8123385a7b1913419127c1c02a3cb47142
fixed deps;

diff -r 9e081c812338 -r b643f4d7b9e9 src/HOL/Induct/Acc.thy
--- a/src/HOL/Induct/Acc.thy	Wed Jun 21 15:58:23 2000 +0200
+++ b/src/HOL/Induct/Acc.thy	Wed Jun 21 18:09:09 2000 +0200
@@ -9,12 +9,12 @@
 Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
 *)
 
-header {* The accessible part of a relation *};
+header {* The accessible part of a relation *}
 
-theory Acc = WF + Inductive:;
+theory Acc = Main:
 
 consts
-  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *};
+  acc  :: "('a * 'a)set => 'a set"  -- {* accessible part *}
 
 inductive "acc r"
   intrs
diff -r 9e081c812338 -r b643f4d7b9e9 src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Wed Jun 21 15:58:23 2000 +0200
+++ b/src/HOL/Induct/Comb.thy	Wed Jun 21 18:09:09 2000 +0200
@@ -13,7 +13,7 @@
 *)
 
 
-Comb = Datatype +
+Comb = Main +
 
 (** Datatype definition of combinators S and K, with infixed application **)
 datatype comb = K
diff -r 9e081c812338 -r b643f4d7b9e9 src/HOL/Induct/LFilter.thy
--- a/src/HOL/Induct/LFilter.thy	Wed Jun 21 15:58:23 2000 +0200
+++ b/src/HOL/Induct/LFilter.thy	Wed Jun 21 18:09:09 2000 +0200
@@ -7,7 +7,7 @@
   --defined by a combination of induction and coinduction
 *)
 
-LFilter = LList + Relation +
+LFilter = LList +
 
 consts
   findRel	:: "('a => bool) => ('a llist * 'a llist)set"
diff -r 9e081c812338 -r b643f4d7b9e9 src/HOL/Induct/Perm.thy
--- a/src/HOL/Induct/Perm.thy	Wed Jun 21 15:58:23 2000 +0200
+++ b/src/HOL/Induct/Perm.thy	Wed Jun 21 18:09:09 2000 +0200
@@ -6,7 +6,7 @@
 Permutations: example of an inductive definition
 *)
 
-Perm = List +
+Perm = Main +
 
 consts  perm    :: "('a list * 'a list) set"   
 syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
diff -r 9e081c812338 -r b643f4d7b9e9 src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Wed Jun 21 15:58:23 2000 +0200
+++ b/src/HOL/Induct/PropLog.ML	Wed Jun 21 18:09:09 2000 +0200
@@ -58,15 +58,15 @@
 
 (** The function eval **)
 
-Goalw [eval_def] "tt[false] = False";
+Goalw [eval_def] "tt[[false]] = False";
 by (Simp_tac 1);
 qed "eval_false";
 
-Goalw [eval_def] "tt[#v] = (v:tt)";
+Goalw [eval_def] "tt[[#v]] = (v:tt)";
 by (Simp_tac 1);
 qed "eval_var";
 
-Goalw [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
+Goalw [eval_def] "tt[[p->q]] = (tt[[p]]-->tt[[q]])";
 by (Simp_tac 1);
 qed "eval_imp";
 
@@ -98,7 +98,7 @@
 qed "imp_false";
 
 (*This formulation is required for strong induction hypotheses*)
-Goal "hyps p tt |- (if tt[p] then p else p->false)";
+Goal "hyps p tt |- (if tt[[p]] then p else p->false)";
 by (rtac (split_if RS iffD2) 1);
 by (induct_tac "p" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
diff -r 9e081c812338 -r b643f4d7b9e9 src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Wed Jun 21 15:58:23 2000 +0200
+++ b/src/HOL/Induct/PropLog.thy	Wed Jun 21 18:09:09 2000 +0200
@@ -6,7 +6,7 @@
 Inductive definition of propositional logic.
 *)
 
-PropLog = Finite + Datatype +
+PropLog = Main +
 
 datatype
     'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
@@ -15,7 +15,7 @@
   "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
   "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
   eval2 :: ['a pl, 'a set] => bool
-  eval  :: ['a set, 'a pl] => bool      ("_[_]" [100,0] 100)
+  eval  :: ['a set, 'a pl] => bool      ("_[[_]]" [100,0] 100)
   hyps  :: ['a pl, 'a set] => 'a pl set
 
 translations
@@ -30,8 +30,8 @@
   MP  "[| H |- p->q; H |- p |] ==> H |- q"
 
 defs
-  sat_def  "H |= p  ==  (!tt. (!q:H. tt[q]) --> tt[p])"
-  eval_def "tt[p] == eval2 p tt"
+  sat_def  "H |= p  ==  (!tt. (!q:H. tt[[q]]) --> tt[[p]])"
+  eval_def "tt[[p]] == eval2 p tt"
 
 primrec
   "eval2(false) = (%x. False)"
diff -r 9e081c812338 -r b643f4d7b9e9 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 21 15:58:23 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 21 18:09:09 2000 +0200
@@ -426,7 +426,7 @@
   ex/Primrec.ML ex/Primrec.thy \
   ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \
   ex/ROOT.ML ex/Recdefs.ML ex/Recdefs.thy ex/cla.ML ex/meson.ML \
-  ex/mesontest.ML ex/mesontest2.ML ex/set.ML \
+  ex/mesontest.ML ex/mesontest2.ML ex/set.thy ex/set.ML \
   ex/Group.ML ex/Group.thy ex/IntRing.ML ex/IntRing.thy \
   ex/Lagrange.ML ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
   ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \