author | haftmann |
Mon, 23 Mar 2009 19:01:15 +0100 | |
changeset 30684 | c98a64746c69 |
parent 30665 | 4cf38ea4fad2 |
child 30685 | dd5fe091ff04 |
--- a/src/HOL/Decision_Procs/Ferrack.thy Mon Mar 23 08:16:24 2009 +0100 +++ b/src/HOL/Decision_Procs/Ferrack.thy Mon Mar 23 19:01:15 2009 +0100 @@ -1995,6 +1995,8 @@ "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0))) (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))" +code_reserved SML oo + ML {* @{code ferrack_test} () *} oracle linr_oracle = {*