Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

wdfs

This commit is contained in:
Burkhart Wolff 2018-11-06 11:05:11 +01:00
parent 46c51235e3
commit 8e216c02f2
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
RegExpInterface.thy
View File

@ -96,9 +96,9 @@ export_code zero one Suc Int.nat nat_of_integer int_of_integer (* for debuggi
in SML module_name RegExpChecker file "RegExpChecker.sml"
(*
SML_file "RegExpChecker.sml"
*)
section\<open>The Abstract Interface For Monitor Expressions\<close>
text\<open>Here comes the hic : The reflection of the HOL-Automata module into an SML module
with an abstract interface hiding some generation artefacts like the internal states

2
examples/scholarly/Monitor_Example.thy
View File

@ -16,7 +16,7 @@ val term = @{term "(title ~~
ML\<open>
val alpha = (RegExpInterface.alphabet [term]);
val DA as (init,(next,fin)) = RegExpInterface.rexp_term2da (RegExpInterface.alphabet [term]) term ;
val DA as (init,(next,fin)) = RegExpInterface.rexp_term2da alpha term ;
RegExpChecker.accepts DA [0,2,3,4,5,6,7,8];
\<close>