Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updating to new notation in commented examples
authorbulwahn
Fri, 22 Oct 2010 18:38:59 +0200
changeset 40100 98d74bbe8cd8
parent 40075 1c75f3f192ae
child 40101 f7fc517e21c6
updating to new notation in commented examples
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Oct 22 17:15:46 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Fri Oct 22 18:38:59 2010 +0200
@@ -70,14 +70,13 @@
 where
   "False \<Longrightarrow> False''"
 
-code_pred (expected_modes: []) False'' .
+code_pred (expected_modes: bool) False'' .
 
 inductive EmptySet'' :: "'a \<Rightarrow> bool"
 where
   "False \<Longrightarrow> EmptySet'' x"
 
-code_pred (expected_modes: [1]) EmptySet'' .
-code_pred (expected_modes: [], [1]) [inductify] EmptySet'' .
+code_pred (expected_modes: i => bool, o => bool) [inductify] EmptySet'' .
 *)
 
 consts a' :: 'a
isabelle