src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
changeset 46752 e9e7209eb375
parent 45970 b6d0cff57d96
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Mar 01 17:13:54 2012 +0000
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Mar 01 19:34:52 2012 +0100
     1.3 @@ -1043,14 +1043,14 @@
     1.4    (i => bool) => o * i => bool,
     1.5    (i => bool) => i => bool) [inductify] Id_on .
     1.6  thm Id_on.equation
     1.7 -thm Domain_def
     1.8 +thm Domain_unfold
     1.9  code_pred (modes:
    1.10    (o * o => bool) => o => bool,
    1.11    (o * o => bool) => i => bool,
    1.12    (i * o => bool) => i => bool) [inductify] Domain .
    1.13  thm Domain.equation
    1.14  
    1.15 -thm Range_def
    1.16 +thm Domain_converse [symmetric]
    1.17  code_pred (modes:
    1.18    (o * o => bool) => o => bool,
    1.19    (o * o => bool) => i => bool,