--- a/src/Doc/Datatypes/Datatypes.thy Mon Oct 07 08:39:50 2013 -0700
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Oct 07 20:34:14 2013 +0200
@@ -1800,8 +1800,8 @@
function translates a DFA into a @{type state_machine}:
*}
- primcorec (*<*)(in early) (*>*)
- sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
+ primcorec
+ (*<*)(in early) (*>*)sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine"
where
"sm_of_dfa \<delta> F q = State_Machine (q \<in> F) (sm_of_dfa \<delta> F o \<delta> q)"