--- a/ProgTutorial/Essential.thy Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Essential.thy Wed Feb 23 23:55:37 2011 +0000
@@ -1704,7 +1704,7 @@
val thm = @{thm foo_test1}
val meta_eq = Object_Logic.atomize (cprop_of thm)
in
- MetaSimplifier.rewrite_rule [meta_eq] thm
+ Raw_Simplifier.rewrite_rule [meta_eq] thm
end"
"?A \<longrightarrow> ?B \<longrightarrow> ?C"}
@@ -1728,7 +1728,7 @@
val thm' = forall_intr_vars thm
val thm'' = Object_Logic.atomize (cprop_of thm')
in
- MetaSimplifier.rewrite_rule [thm''] thm'
+ Raw_Simplifier.rewrite_rule [thm''] thm'
end*}
text {*
--- a/ProgTutorial/First_Steps.thy Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/First_Steps.thy Wed Feb 23 23:55:37 2011 +0000
@@ -158,34 +158,6 @@
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
- It is also possible to redirect the ``channel'' where the string @{text
- "foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from
- choking on massive amounts of trace output. This redirection can be achieved
- with the code:
-*}
-
-ML{*val strip_specials =
-let
- fun strip ("\^A" :: _ :: cs) = strip cs
- | strip (c :: cs) = c :: strip cs
- | strip [] = [];
-in
- implode o strip o explode
-end
-
-fun redirect_tracing stream =
- Output.Private_Hooks.tracing_fn := (fn s =>
- (TextIO.output (stream, (strip_specials s));
- TextIO.output (stream, "\n");
- TextIO.flushOut stream)) *}
-
-text {*
- Calling now
-
- @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"}
-
- will cause that all tracing information is printed into the file @{text "foo.bar"}.
-
You can print out error messages with the function @{ML_ind error in Library}; for
example:
@@ -900,13 +872,13 @@
ML{*fun get_thm_names_from_ss simpset =
let
- val {simps,...} = MetaSimplifier.dest_ss simpset
+ val {simps,...} = Raw_Simplifier.dest_ss simpset
in
map #1 simps
end*}
text {*
- The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all
+ The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all
information stored in the simpset, but here we are only interested in the names of the
simp-rules. Now you can feed in the current simpset into this function.
The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
--- a/ProgTutorial/Parsing.thy Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Parsing.thy Wed Feb 23 23:55:37 2011 +0000
@@ -90,7 +90,7 @@
In the examples above we use the function @{ML_ind explode in Symbol} from the
structure @{ML_struct Symbol}, instead of the more standard library function
@{ML_ind explode in String}, for obtaining an input list for the parser. The reason is
- that @{ML explode} in @{ML_struct Symbol} is aware of character
+ that @{ML explode in Symbol} is aware of character
sequences, for example @{text "\<foo>"}, that have a special meaning in
Isabelle. To see the difference consider
@@ -98,7 +98,7 @@
"let
val input = \"\<foo> bar\"
in
- (explode input, Symbol.explode input)
+ (String.explode input, Symbol.explode input)
end"
"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
[\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
--- 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]
--- a/ProgTutorial/Solutions.thy Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Solutions.thy Wed Feb 23 23:55:37 2011 +0000
@@ -83,8 +83,8 @@
@{ML_response [display,gray]
"let
- val input1 = (explode \"foo bar\")
- val input2 = (explode \"foo (*test*) bar (*test*)\")
+ val input1 = (Symbol.explode \"foo bar\")
+ val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
in
(scan_all input1, scan_all input2)
end"
--- a/ProgTutorial/Tactical.thy Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Tactical.thy Wed Feb 23 23:55:37 2011 +0000
@@ -1400,7 +1400,7 @@
corresponding preconditions.
\begin{readmore}
- For more information about the simplifier see @{ML_file "Pure/meta_simplifier.ML"}
+ For more information about the simplifier see @{ML_file "Pure/raw_simplifier.ML"}
and @{ML_file "Pure/simplifier.ML"}. The generic splitter is implemented in
@{ML_file "Provers/splitter.ML"}.
\end{readmore}
@@ -1413,9 +1413,9 @@
\begin{isabelle}
\begin{tabular}{l@ {\hspace{10mm}}l}
- @{ML_ind addsimps in MetaSimplifier} & @{ML_ind delsimps in MetaSimplifier}\\
- @{ML_ind addcongs in MetaSimplifier} & @{ML_ind delcongs in MetaSimplifier}\\
- @{ML_ind addsimprocs in MetaSimplifier} & @{ML_ind delsimprocs in MetaSimplifier}\\
+ @{ML_ind addsimps in Raw_Simplifier} & @{ML_ind delsimps in Raw_Simplifier}\\
+ @{ML_ind addcongs in Raw_Simplifier} & @{ML_ind delcongs in Raw_Simplifier}\\
+ @{ML_ind addsimprocs in Raw_Simplifier} & @{ML_ind delsimprocs in Raw_Simplifier}\\
\end{tabular}
\end{isabelle}
@@ -1428,7 +1428,7 @@
\begin{isabelle}*}
ML{*fun print_ss ctxt ss =
let
- val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
+ val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
fun name_thm (nm, thm) =
Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
@@ -1445,7 +1445,7 @@
text_raw {*
\end{isabelle}
\end{minipage}
-\caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing
+\caption{The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing
all printable information stored in a simpset. We are here only interested in the
simplification rules, congruence rules and simprocs.\label{fig:printss}}
\end{figure} *}
@@ -1454,7 +1454,7 @@
text {*
To see how they work, consider the function in Figure~\ref{fig:printss}, which
prints out some parts of a simpset. If you use it to print out the components of the
- empty simpset, i.e., @{ML_ind empty_ss in MetaSimplifier}
+ empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
@{ML_response_fake [display,gray]
"print_ss @{context} empty_ss"
@@ -1559,7 +1559,7 @@
\end{readmore}
The simplifier is often used to unfold definitions in a proof. For this the
- simplifier implements the tactic @{ML_ind rewrite_goal_tac in MetaSimplifier}.\footnote{\bf FIXME:
+ simplifier implements the tactic @{ML_ind rewrite_goal_tac in Raw_Simplifier}.\footnote{\bf FIXME:
see LocalDefs infrastructure.} Suppose for example the
definition
*}
@@ -1581,7 +1581,7 @@
text {*
If you want to unfold definitions in \emph{all} subgoals, not just one,
- then use the the tactic @{ML_ind rewrite_goals_tac in MetaSimplifier}.
+ then use the the tactic @{ML_ind rewrite_goals_tac in Raw_Simplifier}.
*}
@@ -1871,7 +1871,7 @@
Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
The function also takes a list of patterns that can trigger the simproc.
Now the simproc is set up and can be explicitly added using
- @{ML_ind addsimprocs in MetaSimplifier} to a simpset whenever
+ @{ML_ind addsimprocs in Raw_Simplifier} to a simpset whenever
needed.
Simprocs are applied from inside to outside and from left to right. You can
@@ -2539,7 +2539,7 @@
See @{ML_file "Pure/conv.ML"}
for more information about conversion combinators.
Some basic conversions are defined in @{ML_file "Pure/thm.ML"},
- @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}.
+ @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/raw_simplifier.ML"}.
\end{readmore}
*}
--- a/ProgTutorial/document/root.tex Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/document/root.tex Wed Feb 23 23:55:37 2011 +0000
@@ -153,7 +153,7 @@
\title{\mbox{}\\[-10ex]
\includegraphics[scale=0.5]{tutorial-logo.jpg}\\[3ex]
{\huge\bf The Isabelle Cookbook}\\
- \mbox{A Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)}
+ \mbox{A Gentle Tutorial for Programming on the ML-Level of Isabelle}\\ (draft)}
\author{by Christian Urban with contributions from:\\[2ex]
\begin{tabular}{r@{\hspace{1.8mm}}l}
Binary file progtutorial.pdf has changed