equal
deleted
inserted
replaced
19 "~~/src/Tools/Code/code_target.ML" |
19 "~~/src/Tools/Code/code_target.ML" |
20 "~~/src/Tools/Code/code_namespace.ML" |
20 "~~/src/Tools/Code/code_namespace.ML" |
21 "~~/src/Tools/Code/code_ml.ML" |
21 "~~/src/Tools/Code/code_ml.ML" |
22 "~~/src/Tools/Code/code_haskell.ML" |
22 "~~/src/Tools/Code/code_haskell.ML" |
23 "~~/src/Tools/Code/code_scala.ML" |
23 "~~/src/Tools/Code/code_scala.ML" |
24 "~~/src/Tools/Code/code_runtime.ML" |
|
25 "~~/src/Tools/nbe.ML" |
24 "~~/src/Tools/nbe.ML" |
|
25 ("~~/src/Tools/Code/code_runtime.ML") |
26 begin |
26 begin |
27 |
27 |
28 setup {* |
28 setup {* |
29 Auto_Solve.setup |
29 Auto_Solve.setup |
30 #> Code_Preproc.setup |
30 #> Code_Preproc.setup |
31 #> Code_Simp.setup |
31 #> Code_Simp.setup |
32 #> Code_ML.setup |
32 #> Code_ML.setup |
33 #> Code_Haskell.setup |
33 #> Code_Haskell.setup |
34 #> Code_Scala.setup |
34 #> Code_Scala.setup |
35 #> Code_Runtime.setup |
|
36 #> Nbe.setup |
35 #> Nbe.setup |
37 #> Quickcheck.setup |
36 #> Quickcheck.setup |
38 *} |
37 *} |
39 |
38 |
40 code_datatype "TYPE('a\<Colon>{})" |
39 code_datatype "TYPE('a\<Colon>{})" |
62 next |
61 next |
63 show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds" |
62 show "(PROP P \<Longrightarrow> PROP holds) \<equiv> PROP holds" |
64 by rule (rule holds)+ |
63 by rule (rule holds)+ |
65 qed |
64 qed |
66 |
65 |
|
66 use "~~/src/Tools/Code/code_runtime.ML" |
|
67 |
67 hide_const (open) holds |
68 hide_const (open) holds |
68 |
69 |
69 end |
70 end |