# HG changeset patch
# User wenzelm
# Date 956010962 -7200
# Node ID aef229ca5e77aebf67ea02540a4cdb0f9a992dfa
# Parent  085f0e32b9d61f65f6743acd28b5e431f7b4aade
fixed theory deps;

diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/AutoChopper1.thy
--- a/src/HOL/Lex/AutoChopper1.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/AutoChopper1.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -17,7 +17,7 @@
 No proofs yet.
 *)
 
-AutoChopper1 = DA + Chopper + Main +
+AutoChopper1 = DA + Chopper +
 
 consts
   acc :: "(('a,'s)da * 'a list * 's * 'a list list * 'a list * 'a list)
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/AutoProj.thy
--- a/src/HOL/Lex/AutoProj.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/AutoProj.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -9,7 +9,7 @@
 and use foldl instead of foldl2.
 *)
 
-AutoProj = Prod +
+AutoProj = Main +
 
 constdefs
  start :: "'a * 'b * 'c => 'a"
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/DA.thy
--- a/src/HOL/Lex/DA.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/DA.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Deterministic automata
 *)
 
-DA = List + AutoProj +
+DA = AutoProj +
 
 types ('a,'s)da = "'s * ('a => 's => 's) * ('s => bool)"
 
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/MaxChop.thy
--- a/src/HOL/Lex/MaxChop.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/MaxChop.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -4,7 +4,7 @@
     Copyright   1998 TUM
 *)
 
-MaxChop = MaxPrefix + Recdef +
+MaxChop = MaxPrefix +
 
 types   'a chopper = "'a list => 'a list list * 'a list"
 
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/NA.thy
--- a/src/HOL/Lex/NA.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/NA.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Nondeterministic automata
 *)
 
-NA = List + AutoProj +
+NA = AutoProj +
 
 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
 
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/NAe.thy
--- a/src/HOL/Lex/NAe.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/NAe.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Nondeterministic automata with epsilon transitions
 *)
 
-NAe = List + Option + NA +
+NAe = NA +
 
 types ('a,'s)nae = ('a option,'s)na
 
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/ROOT.ML
--- a/src/HOL/Lex/ROOT.ML	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/ROOT.ML	Tue Apr 18 00:36:02 2000 +0200
@@ -7,11 +7,5 @@
 use_thy"AutoChopper";
 use_thy"AutoChopper1";
 use_thy"AutoMaxChop";
-(* Do not swap the next two use_thy's.
-   There is some interference, probably via claset() or simpset().
-   Or via ML-bound names of axioms that are overwritten?
-*)
 use_thy"RegSet_of_nat_DA";
-use_thy"RegExp2NA";
-use_thy"RegExp2NAe";
 use_thy"Scanner";
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/RegExp2NA.thy
--- a/src/HOL/Lex/RegExp2NA.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/RegExp2NA.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -7,7 +7,7 @@
 into nondeterministic automata *without* epsilon transitions
 *)
 
-RegExp2NA = NA + RegExp +
+RegExp2NA = RegExp + NA +
 
 types 'a bitsNA = ('a,bool list)na
 
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/RegExp2NAe.thy
--- a/src/HOL/Lex/RegExp2NAe.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/RegExp2NAe.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -7,7 +7,7 @@
 into nondeterministic automata with epsilon transitions
 *)
 
-RegExp2NAe = NAe + RegExp +
+RegExp2NAe = RegExp + NAe +
 
 types 'a bitsNAe = ('a,bool list)nae
 
diff -r 085f0e32b9d6 -r aef229ca5e77 src/HOL/Lex/RegSet.thy
--- a/src/HOL/Lex/RegSet.thy	Mon Apr 17 14:27:10 2000 +0200
+++ b/src/HOL/Lex/RegSet.thy	Tue Apr 18 00:36:02 2000 +0200
@@ -6,7 +6,7 @@
 Regular sets
 *)
 
-RegSet = List +
+RegSet = Main +
 
 constdefs
  conc :: 'a list set => 'a list set => 'a list set