be explicit about .ML files;
authorwenzelm
Wed Oct 24 19:21:40 2007 +0200 (2007-10-24)
changeset 25174d70d6dbc3a60
parent 25173 7e1f197a36c5
child 25175 66a33a664609
be explicit about .ML files;
src/HOL/Statespace/DistinctTreeProver.thy
src/HOL/Statespace/StateFun.thy
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/Statespace/document/root.tex
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Wed Oct 24 19:21:39 2007 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Wed Oct 24 19:21:40 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory DistinctTreeProver 
     1.6  imports Main
     1.7 -uses (distinct_tree_prover)
     1.8 +uses ("distinct_tree_prover.ML")
     1.9  begin
    1.10  
    1.11  text {* A state space manages a set of (abstract) names and assumes
    1.12 @@ -632,7 +632,7 @@
    1.13  text {* Now we have all the theorems in place that are needed for the
    1.14  certificate generating ML functions. *}
    1.15  
    1.16 -use distinct_tree_prover
    1.17 +use "distinct_tree_prover.ML"
    1.18  
    1.19  (* Uncomment for profiling or debugging *)
    1.20  (*
     2.1 --- a/src/HOL/Statespace/StateFun.thy	Wed Oct 24 19:21:39 2007 +0200
     2.2 +++ b/src/HOL/Statespace/StateFun.thy	Wed Oct 24 19:21:40 2007 +0200
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* State Space Representation as Function \label{sec:StateFun}*}
     2.5  
     2.6  theory StateFun imports DistinctTreeProver 
     2.7 -(*uses "state_space.ML" (state_fun)*)
     2.8 +(*uses "state_space.ML" ("state_fun.ML")*)
     2.9  begin
    2.10  
    2.11  
    2.12 @@ -109,7 +109,7 @@
    2.13    apply simp
    2.14    oops
    2.15  
    2.16 -(*use "state_fun"
    2.17 +(*use "state_fun.ML"
    2.18  setup StateFun.setup
    2.19  *)
    2.20  end
    2.21 \ No newline at end of file
     3.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Wed Oct 24 19:21:39 2007 +0200
     3.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Wed Oct 24 19:21:40 2007 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
     3.5  
     3.6  theory StateSpaceLocale imports StateFun 
     3.7 -uses "state_space.ML" "state_fun"
     3.8 +uses "state_space.ML" "state_fun.ML"
     3.9  begin
    3.10  
    3.11  setup StateFun.setup
     4.1 --- a/src/HOL/Statespace/document/root.tex	Wed Oct 24 19:21:39 2007 +0200
     4.2 +++ b/src/HOL/Statespace/document/root.tex	Wed Oct 24 19:21:40 2007 +0200
     4.3 @@ -42,7 +42,7 @@
     4.4  
     4.5  \tableofcontents
     4.6  
     4.7 -%\parindent 0pt\parskip 0.5ex
     4.8 +\parindent 0pt\parskip 0.5ex
     4.9  
    4.10  \section{Introduction}
    4.11