# HG changeset patch
# User bulwahn
# Date 1287765539 -7200
# Node ID 98d74bbe8cd8b99318170f5abbb20501c49c2259
# Parent  1c75f3f192ae30b09bb9c1758484da4eb58cc11e
updating to new notation in commented examples

diff -r 1c75f3f192ae -r 98d74bbe8cd8 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- 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