# HG changeset patch # User bulwahn # Date 1284967578 -7200 # Node ID 9ff9651757cd1d5887658a8e3969098027b0bf99 # Parent a50c0ae2312c789015055a2d4990121ebf9674bc removing unnessary options for code_pred diff -r a50c0ae2312c -r 9ff9651757cd src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Sep 20 09:26:16 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Mon Sep 20 09:26:18 2010 +0200 @@ -1612,13 +1612,13 @@ rule ''A'' [TS ''b'']}, ''S'')" -code_pred [inductify,skip_proof] derives . +code_pred [inductify, skip_proof] derives . thm derives.equation definition "test = { rhs. derives example_grammar ([NTS ''S''], rhs) }" -code_pred (modes: o \ bool) [inductify, show_modes, show_intermediate_results, skip_proof] test . +code_pred (modes: o \ bool) [inductify] test . thm test.equation values "{rhs. test rhs}"