--- a/src/HOL/Statespace/DistinctTreeProver.thy Wed Oct 24 19:21:39 2007 +0200
+++ b/src/HOL/Statespace/DistinctTreeProver.thy Wed Oct 24 19:21:40 2007 +0200
@@ -7,7 +7,7 @@
theory DistinctTreeProver
imports Main
-uses (distinct_tree_prover)
+uses ("distinct_tree_prover.ML")
begin
text {* A state space manages a set of (abstract) names and assumes
@@ -632,7 +632,7 @@
text {* Now we have all the theorems in place that are needed for the
certificate generating ML functions. *}
-use distinct_tree_prover
+use "distinct_tree_prover.ML"
(* Uncomment for profiling or debugging *)
(*
--- a/src/HOL/Statespace/StateFun.thy Wed Oct 24 19:21:39 2007 +0200
+++ b/src/HOL/Statespace/StateFun.thy Wed Oct 24 19:21:40 2007 +0200
@@ -6,7 +6,7 @@
header {* State Space Representation as Function \label{sec:StateFun}*}
theory StateFun imports DistinctTreeProver
-(*uses "state_space.ML" (state_fun)*)
+(*uses "state_space.ML" ("state_fun.ML")*)
begin
@@ -109,7 +109,7 @@
apply simp
oops
-(*use "state_fun"
+(*use "state_fun.ML"
setup StateFun.setup
*)
end
\ No newline at end of file
--- a/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 24 19:21:39 2007 +0200
+++ b/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 24 19:21:40 2007 +0200
@@ -6,7 +6,7 @@
header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
theory StateSpaceLocale imports StateFun
-uses "state_space.ML" "state_fun"
+uses "state_space.ML" "state_fun.ML"
begin
setup StateFun.setup
--- a/src/HOL/Statespace/document/root.tex Wed Oct 24 19:21:39 2007 +0200
+++ b/src/HOL/Statespace/document/root.tex Wed Oct 24 19:21:40 2007 +0200
@@ -42,7 +42,7 @@
\tableofcontents
-%\parindent 0pt\parskip 0.5ex
+\parindent 0pt\parskip 0.5ex
\section{Introduction}