--- a/ProgTutorial/Recipes/Sat.thy	Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Wed Feb 23 23:55:37 2011 +0000
@@ -18,22 +18,22 @@
   The SAT solvers expect a propositional formula as input and produce
   a result indicating that the formula is either satisfiable, unsatisfiable or
   unknown. The type of the propositional formula is  
-  @{ML_type "PropLogic.prop_formula"} with the usual constructors such 
-  as @{ML And in PropLogic}, @{ML Or in PropLogic} and so on.
+  @{ML_type "Prop_Logic.prop_formula"} with the usual constructors such 
+  as @{ML And in Prop_Logic}, @{ML Or in Prop_Logic} and so on.
 
-  The function  @{ML  PropLogic.prop_formula_of_term} translates an Isabelle 
+  The function  @{ML  Prop_Logic.prop_formula_of_term} translates an Isabelle 
   term into a propositional formula. Let
   us illustrate this function by translating @{term "A \<and> \<not>A \<or> B"}. 
   The function will return a propositional formula and a table. Suppose 
 *}
 
 ML{*val (pform, table) = 
-       PropLogic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}
+       Prop_Logic.prop_formula_of_term @{term "A \<and> \<not>A \<or> B"}  Termtab.empty*}
 
 text {*
   then the resulting propositional formula @{ML pform} is 
   
-  @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in PropLogic} 
+  @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} 
   
 
   where indices are assigned for the variables 
@@ -52,10 +52,10 @@
 *}
 
 ML{*val (pform', table') = 
-       PropLogic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}
+       Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty*}
 
 text {*
-  returns @{ML "BoolVar 1" in PropLogic} for  @{ML pform'} and the table 
+  returns @{ML "BoolVar 1" in Prop_Logic} for  @{ML pform'} and the table 
   @{ML table'} is:
 
   @{ML_response_fake [display,gray]