# HG changeset patch
# User wenzelm
# Date 1193246500 -7200
# Node ID d70d6dbc3a60890d6608f27cc548895d354cb7ad
# Parent  7e1f197a36c539bcc11697a54a01bf894bdd6357
be explicit about .ML files;

diff -r 7e1f197a36c5 -r d70d6dbc3a60 src/HOL/Statespace/DistinctTreeProver.thy
--- 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 *)
 (*
diff -r 7e1f197a36c5 -r d70d6dbc3a60 src/HOL/Statespace/StateFun.thy
--- 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
diff -r 7e1f197a36c5 -r d70d6dbc3a60 src/HOL/Statespace/StateSpaceLocale.thy
--- 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
diff -r 7e1f197a36c5 -r d70d6dbc3a60 src/HOL/Statespace/document/root.tex
--- 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}