--- 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
--- 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
--- 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"
--- 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)
--- 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])));
--- 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)"
--- 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 \